(0) Obligation:

Clauses:

mergesort([], [], Ls).
mergesort(.(X, []), .(X, []), Ls).
mergesort(.(X, .(Y, Xs)), Ys, .(H, Ls)) :- ','(split(.(X, .(Y, Xs)), X1s, X2s, .(H, Ls)), ','(mergesort(X1s, Y1s, Ls), ','(mergesort(X2s, Y2s, Ls), merge(Y1s, Y2s, Ys, .(H, Ls))))).
split([], [], [], Ls).
split(.(X, Xs), .(X, Ys), Zs, .(H, Ls)) :- split(Xs, Zs, Ys, Ls).
merge([], Xs, Xs, Ls).
merge(Xs, [], Xs, Ls).
merge(.(X, Xs), .(Y, Ys), .(X, Zs), .(H, Ls)) :- ','(le(X, Y), merge(Xs, .(Y, Ys), Zs, Ls)).
merge(.(X, Xs), .(Y, Ys), .(Y, Zs), .(H, Ls)) :- ','(gt(X, Y), merge(.(X, Xs), Ys, Zs, Ls)).
gt(s(X), s(Y)) :- gt(X, Y).
gt(s(0), 0).
le(s(X), s(Y)) :- le(X, Y).
le(0, s(0)).
le(0, 0).

Query: mergesort(g,a,a)

(1) PrologToDTProblemTransformerProof (SOUND transformation)

Built DT problem from termination graph DT10.

(2) Obligation:

Triples:

splitA(.(X1, X2), .(X1, X3), X4, .(X5, X6)) :- splitA(X2, X4, X3, X6).
splitD(X1, X2, .(X1, X3), X4, .(X5, X6)) :- splitA(X2, X4, X3, X6).
mergesortE(.(X1, .(X2, X3)), X4, .(X5, X6)) :- splitD(X1, .(X2, X3), X7, X8, .(X5, X6)).
mergesortE(.(X1, .(X2, X3)), X4, .(X5, X6)) :- ','(splitcD(X1, .(X2, X3), X7, X8, .(X5, X6)), mergesortE(X7, X9, X6)).
mergesortE(.(X1, .(X2, X3)), X4, .(X5, X6)) :- ','(splitcD(X1, .(X2, X3), X7, X8, .(X5, X6)), ','(mergesortcE(X7, X9, X6), mergesortE(X8, X10, X6))).
mergesortE(.(X1, .(X2, X3)), X4, .(X5, X6)) :- ','(splitcD(X1, .(X2, X3), X7, X8, .(X5, X6)), ','(mergesortcE(X7, X9, X6), ','(mergesortcE(X8, X10, X6), mergeC(X9, X10, X4, X5, X6)))).
mergeC(.(X1, X2), .(X3, X4), .(X1, X5), X6, X7) :- pF(X1, X3, X2, X4, X5, X7).
mergeC(.(X1, X2), .(X3, X4), .(X3, X5), X6, X7) :- pG(X1, X3, X2, X4, X5, X7).
leH(s(X1), s(X2)) :- leH(X1, X2).
pF(X1, X2, X3, X4, X5, X6) :- leH(X1, X2).
pF(X1, X2, .(X3, X4), X5, .(X3, X6), .(X7, X8)) :- ','(lecH(X1, X2), pF(X3, X2, X4, X5, X6, X8)).
pF(X1, X2, .(X3, X4), X5, .(X2, X6), .(X7, X8)) :- ','(lecH(X1, X2), pG(X3, X2, X4, X5, X6, X8)).
gtI(s(X1), s(X2)) :- gtI(X1, X2).
pG(X1, X2, X3, X4, X5, X6) :- gtI(X1, X2).
pG(X1, X2, X3, .(X4, X5), .(X1, X6), .(X7, X8)) :- ','(gtcI(X1, X2), pF(X1, X4, X3, X5, X6, X8)).
pG(X1, X2, X3, .(X4, X5), .(X4, X6), .(X7, X8)) :- ','(gtcI(X1, X2), pG(X1, X4, X3, X5, X6, X8)).
mergesortB(.(X1, .(X2, X3)), X4, .(X5, X6)) :- splitD(X2, X3, X7, X8, X6).
mergesortB(.(X1, .(X2, X3)), X4, .(X5, X6)) :- ','(splitcD(X2, X3, X7, X8, X6), mergesortB(.(X1, X8), X9, X6)).
mergesortB(.(X1, .(X2, X3)), X4, .(X5, X6)) :- ','(splitcD(X2, X3, X7, X8, X6), ','(mergesortcB(.(X1, X8), X9, X6), mergesortE(X7, X10, X6))).
mergesortB(.(X1, .(X2, X3)), X4, .(X5, X6)) :- ','(splitcD(X2, X3, X7, X8, X6), ','(mergesortcB(.(X1, X8), X9, X6), ','(mergesortcE(X7, X10, X6), mergeC(X9, X10, X4, X5, X6)))).

Clauses:

splitcA([], [], [], X1).
splitcA(.(X1, X2), .(X1, X3), X4, .(X5, X6)) :- splitcA(X2, X4, X3, X6).
mergesortcB([], [], X1).
mergesortcB(.(X1, []), .(X1, []), X2).
mergesortcB(.(X1, .(X2, X3)), X4, .(X5, X6)) :- ','(splitcD(X2, X3, X7, X8, X6), ','(mergesortcB(.(X1, X8), X9, X6), ','(mergesortcE(X7, X10, X6), mergecC(X9, X10, X4, X5, X6)))).
splitcD(X1, X2, .(X1, X3), X4, .(X5, X6)) :- splitcA(X2, X4, X3, X6).
mergesortcE([], [], X1).
mergesortcE(.(X1, []), .(X1, []), X2).
mergesortcE(.(X1, .(X2, X3)), X4, .(X5, X6)) :- ','(splitcD(X1, .(X2, X3), X7, X8, .(X5, X6)), ','(mergesortcE(X7, X9, X6), ','(mergesortcE(X8, X10, X6), mergecC(X9, X10, X4, X5, X6)))).
mergecC([], X1, X1, X2, X3).
mergecC(X1, [], X1, X2, X3).
mergecC(.(X1, X2), .(X3, X4), .(X1, X5), X6, X7) :- qcF(X1, X3, X2, X4, X5, X7).
mergecC(.(X1, X2), .(X3, X4), .(X3, X5), X6, X7) :- qcG(X1, X3, X2, X4, X5, X7).
lecH(s(X1), s(X2)) :- lecH(X1, X2).
lecH(0, s(0)).
lecH(0, 0).
qcF(X1, X2, [], X3, .(X2, X3), X4) :- lecH(X1, X2).
qcF(X1, X2, .(X3, X4), X5, .(X3, X6), .(X7, X8)) :- ','(lecH(X1, X2), qcF(X3, X2, X4, X5, X6, X8)).
qcF(X1, X2, .(X3, X4), X5, .(X2, X6), .(X7, X8)) :- ','(lecH(X1, X2), qcG(X3, X2, X4, X5, X6, X8)).
gtcI(s(X1), s(X2)) :- gtcI(X1, X2).
gtcI(s(0), 0).
qcG(X1, X2, X3, [], .(X1, X3), X4) :- gtcI(X1, X2).
qcG(X1, X2, X3, .(X4, X5), .(X1, X6), .(X7, X8)) :- ','(gtcI(X1, X2), qcF(X1, X4, X3, X5, X6, X8)).
qcG(X1, X2, X3, .(X4, X5), .(X4, X6), .(X7, X8)) :- ','(gtcI(X1, X2), qcG(X1, X4, X3, X5, X6, X8)).

Afs:

mergesortB(x1, x2, x3)  =  mergesortB(x1)

(3) TriplesToPiDPProof (SOUND transformation)

We use the technique of [DT09]. With regard to the inferred argument filtering the predicates were used in the following modes:
mergesortB_in: (b,f,f)
splitD_in: (b,b,f,f,f)
splitA_in: (b,f,f,f)
splitcD_in: (b,b,f,f,f)
splitcA_in: (b,f,f,f)
mergesortcB_in: (b,f,f)
mergesortcE_in: (b,f,f)
mergecC_in: (b,b,f,f,f)
qcF_in: (b,b,b,b,f,f)
lecH_in: (b,b)
qcG_in: (b,b,b,b,f,f)
gtcI_in: (b,b)
mergesortE_in: (b,f,f)
mergeC_in: (b,b,f,f,f)
pF_in: (b,b,b,b,f,f)
leH_in: (b,b)
pG_in: (b,b,b,b,f,f)
gtI_in: (b,b)
Transforming TRIPLES into the following Term Rewriting System:
Pi DP problem:
The TRS P consists of the following rules:

MERGESORTB_IN_GAA(.(X1, .(X2, X3)), X4, .(X5, X6)) → U24_GAA(X1, X2, X3, X4, X5, X6, splitD_in_ggaaa(X2, X3, X7, X8, X6))
MERGESORTB_IN_GAA(.(X1, .(X2, X3)), X4, .(X5, X6)) → SPLITD_IN_GGAAA(X2, X3, X7, X8, X6)
SPLITD_IN_GGAAA(X1, X2, .(X1, X3), X4, .(X5, X6)) → U2_GGAAA(X1, X2, X3, X4, X5, X6, splitA_in_gaaa(X2, X4, X3, X6))
SPLITD_IN_GGAAA(X1, X2, .(X1, X3), X4, .(X5, X6)) → SPLITA_IN_GAAA(X2, X4, X3, X6)
SPLITA_IN_GAAA(.(X1, X2), .(X1, X3), X4, .(X5, X6)) → U1_GAAA(X1, X2, X3, X4, X5, X6, splitA_in_gaaa(X2, X4, X3, X6))
SPLITA_IN_GAAA(.(X1, X2), .(X1, X3), X4, .(X5, X6)) → SPLITA_IN_GAAA(X2, X4, X3, X6)
MERGESORTB_IN_GAA(.(X1, .(X2, X3)), X4, .(X5, X6)) → U25_GAA(X1, X2, X3, X4, X5, X6, splitcD_in_ggaaa(X2, X3, X7, X8, X6))
U25_GAA(X1, X2, X3, X4, X5, X6, splitcD_out_ggaaa(X2, X3, X7, X8, X6)) → U26_GAA(X1, X2, X3, X4, X5, X6, mergesortB_in_gaa(.(X1, X8), X9, X6))
U25_GAA(X1, X2, X3, X4, X5, X6, splitcD_out_ggaaa(X2, X3, X7, X8, X6)) → MERGESORTB_IN_GAA(.(X1, X8), X9, X6)
U25_GAA(X1, X2, X3, X4, X5, X6, splitcD_out_ggaaa(X2, X3, X7, X8, X6)) → U27_GAA(X1, X2, X3, X4, X5, X6, X7, mergesortcB_in_gaa(.(X1, X8), X9, X6))
U27_GAA(X1, X2, X3, X4, X5, X6, X7, mergesortcB_out_gaa(.(X1, X8), X9, X6)) → U28_GAA(X1, X2, X3, X4, X5, X6, mergesortE_in_gaa(X7, X10, X6))
U27_GAA(X1, X2, X3, X4, X5, X6, X7, mergesortcB_out_gaa(.(X1, X8), X9, X6)) → MERGESORTE_IN_GAA(X7, X10, X6)
MERGESORTE_IN_GAA(.(X1, .(X2, X3)), X4, .(X5, X6)) → U3_GAA(X1, X2, X3, X4, X5, X6, splitD_in_ggaaa(X1, .(X2, X3), X7, X8, .(X5, X6)))
MERGESORTE_IN_GAA(.(X1, .(X2, X3)), X4, .(X5, X6)) → SPLITD_IN_GGAAA(X1, .(X2, X3), X7, X8, .(X5, X6))
MERGESORTE_IN_GAA(.(X1, .(X2, X3)), X4, .(X5, X6)) → U4_GAA(X1, X2, X3, X4, X5, X6, splitcD_in_ggaaa(X1, .(X2, X3), X7, X8, .(X5, X6)))
U4_GAA(X1, X2, X3, X4, X5, X6, splitcD_out_ggaaa(X1, .(X2, X3), X7, X8, .(X5, X6))) → U5_GAA(X1, X2, X3, X4, X5, X6, mergesortE_in_gaa(X7, X9, X6))
U4_GAA(X1, X2, X3, X4, X5, X6, splitcD_out_ggaaa(X1, .(X2, X3), X7, X8, .(X5, X6))) → MERGESORTE_IN_GAA(X7, X9, X6)
U4_GAA(X1, X2, X3, X4, X5, X6, splitcD_out_ggaaa(X1, .(X2, X3), X7, X8, .(X5, X6))) → U6_GAA(X1, X2, X3, X4, X5, X6, X8, mergesortcE_in_gaa(X7, X9, X6))
U6_GAA(X1, X2, X3, X4, X5, X6, X8, mergesortcE_out_gaa(X7, X9, X6)) → U7_GAA(X1, X2, X3, X4, X5, X6, mergesortE_in_gaa(X8, X10, X6))
U6_GAA(X1, X2, X3, X4, X5, X6, X8, mergesortcE_out_gaa(X7, X9, X6)) → MERGESORTE_IN_GAA(X8, X10, X6)
U6_GAA(X1, X2, X3, X4, X5, X6, X8, mergesortcE_out_gaa(X7, X9, X6)) → U8_GAA(X1, X2, X3, X4, X5, X6, X9, mergesortcE_in_gaa(X8, X10, X6))
U8_GAA(X1, X2, X3, X4, X5, X6, X9, mergesortcE_out_gaa(X8, X10, X6)) → U9_GAA(X1, X2, X3, X4, X5, X6, mergeC_in_ggaaa(X9, X10, X4, X5, X6))
U8_GAA(X1, X2, X3, X4, X5, X6, X9, mergesortcE_out_gaa(X8, X10, X6)) → MERGEC_IN_GGAAA(X9, X10, X4, X5, X6)
MERGEC_IN_GGAAA(.(X1, X2), .(X3, X4), .(X1, X5), X6, X7) → U10_GGAAA(X1, X2, X3, X4, X5, X6, X7, pF_in_ggggaa(X1, X3, X2, X4, X5, X7))
MERGEC_IN_GGAAA(.(X1, X2), .(X3, X4), .(X1, X5), X6, X7) → PF_IN_GGGGAA(X1, X3, X2, X4, X5, X7)
PF_IN_GGGGAA(X1, X2, X3, X4, X5, X6) → U13_GGGGAA(X1, X2, X3, X4, X5, X6, leH_in_gg(X1, X2))
PF_IN_GGGGAA(X1, X2, X3, X4, X5, X6) → LEH_IN_GG(X1, X2)
LEH_IN_GG(s(X1), s(X2)) → U12_GG(X1, X2, leH_in_gg(X1, X2))
LEH_IN_GG(s(X1), s(X2)) → LEH_IN_GG(X1, X2)
PF_IN_GGGGAA(X1, X2, .(X3, X4), X5, .(X3, X6), .(X7, X8)) → U14_GGGGAA(X1, X2, X3, X4, X5, X6, X7, X8, lecH_in_gg(X1, X2))
U14_GGGGAA(X1, X2, X3, X4, X5, X6, X7, X8, lecH_out_gg(X1, X2)) → U15_GGGGAA(X1, X2, X3, X4, X5, X6, X7, X8, pF_in_ggggaa(X3, X2, X4, X5, X6, X8))
U14_GGGGAA(X1, X2, X3, X4, X5, X6, X7, X8, lecH_out_gg(X1, X2)) → PF_IN_GGGGAA(X3, X2, X4, X5, X6, X8)
PF_IN_GGGGAA(X1, X2, .(X3, X4), X5, .(X2, X6), .(X7, X8)) → U16_GGGGAA(X1, X2, X3, X4, X5, X6, X7, X8, lecH_in_gg(X1, X2))
U16_GGGGAA(X1, X2, X3, X4, X5, X6, X7, X8, lecH_out_gg(X1, X2)) → U17_GGGGAA(X1, X2, X3, X4, X5, X6, X7, X8, pG_in_ggggaa(X3, X2, X4, X5, X6, X8))
U16_GGGGAA(X1, X2, X3, X4, X5, X6, X7, X8, lecH_out_gg(X1, X2)) → PG_IN_GGGGAA(X3, X2, X4, X5, X6, X8)
PG_IN_GGGGAA(X1, X2, X3, X4, X5, X6) → U19_GGGGAA(X1, X2, X3, X4, X5, X6, gtI_in_gg(X1, X2))
PG_IN_GGGGAA(X1, X2, X3, X4, X5, X6) → GTI_IN_GG(X1, X2)
GTI_IN_GG(s(X1), s(X2)) → U18_GG(X1, X2, gtI_in_gg(X1, X2))
GTI_IN_GG(s(X1), s(X2)) → GTI_IN_GG(X1, X2)
PG_IN_GGGGAA(X1, X2, X3, .(X4, X5), .(X1, X6), .(X7, X8)) → U20_GGGGAA(X1, X2, X3, X4, X5, X6, X7, X8, gtcI_in_gg(X1, X2))
U20_GGGGAA(X1, X2, X3, X4, X5, X6, X7, X8, gtcI_out_gg(X1, X2)) → U21_GGGGAA(X1, X2, X3, X4, X5, X6, X7, X8, pF_in_ggggaa(X1, X4, X3, X5, X6, X8))
U20_GGGGAA(X1, X2, X3, X4, X5, X6, X7, X8, gtcI_out_gg(X1, X2)) → PF_IN_GGGGAA(X1, X4, X3, X5, X6, X8)
PG_IN_GGGGAA(X1, X2, X3, .(X4, X5), .(X4, X6), .(X7, X8)) → U22_GGGGAA(X1, X2, X3, X4, X5, X6, X7, X8, gtcI_in_gg(X1, X2))
U22_GGGGAA(X1, X2, X3, X4, X5, X6, X7, X8, gtcI_out_gg(X1, X2)) → U23_GGGGAA(X1, X2, X3, X4, X5, X6, X7, X8, pG_in_ggggaa(X1, X4, X3, X5, X6, X8))
U22_GGGGAA(X1, X2, X3, X4, X5, X6, X7, X8, gtcI_out_gg(X1, X2)) → PG_IN_GGGGAA(X1, X4, X3, X5, X6, X8)
MERGEC_IN_GGAAA(.(X1, X2), .(X3, X4), .(X3, X5), X6, X7) → U11_GGAAA(X1, X2, X3, X4, X5, X6, X7, pG_in_ggggaa(X1, X3, X2, X4, X5, X7))
MERGEC_IN_GGAAA(.(X1, X2), .(X3, X4), .(X3, X5), X6, X7) → PG_IN_GGGGAA(X1, X3, X2, X4, X5, X7)
U27_GAA(X1, X2, X3, X4, X5, X6, X7, mergesortcB_out_gaa(.(X1, X8), X9, X6)) → U29_GAA(X1, X2, X3, X4, X5, X6, X9, mergesortcE_in_gaa(X7, X10, X6))
U29_GAA(X1, X2, X3, X4, X5, X6, X9, mergesortcE_out_gaa(X7, X10, X6)) → U30_GAA(X1, X2, X3, X4, X5, X6, mergeC_in_ggaaa(X9, X10, X4, X5, X6))
U29_GAA(X1, X2, X3, X4, X5, X6, X9, mergesortcE_out_gaa(X7, X10, X6)) → MERGEC_IN_GGAAA(X9, X10, X4, X5, X6)

The TRS R consists of the following rules:

splitcD_in_ggaaa(X1, X2, .(X1, X3), X4, .(X5, X6)) → U37_ggaaa(X1, X2, X3, X4, X5, X6, splitcA_in_gaaa(X2, X4, X3, X6))
splitcA_in_gaaa([], [], [], X1) → splitcA_out_gaaa([], [], [], X1)
splitcA_in_gaaa(.(X1, X2), .(X1, X3), X4, .(X5, X6)) → U32_gaaa(X1, X2, X3, X4, X5, X6, splitcA_in_gaaa(X2, X4, X3, X6))
U32_gaaa(X1, X2, X3, X4, X5, X6, splitcA_out_gaaa(X2, X4, X3, X6)) → splitcA_out_gaaa(.(X1, X2), .(X1, X3), X4, .(X5, X6))
U37_ggaaa(X1, X2, X3, X4, X5, X6, splitcA_out_gaaa(X2, X4, X3, X6)) → splitcD_out_ggaaa(X1, X2, .(X1, X3), X4, .(X5, X6))
mergesortcB_in_gaa([], [], X1) → mergesortcB_out_gaa([], [], X1)
mergesortcB_in_gaa(.(X1, []), .(X1, []), X2) → mergesortcB_out_gaa(.(X1, []), .(X1, []), X2)
mergesortcB_in_gaa(.(X1, .(X2, X3)), X4, .(X5, X6)) → U33_gaa(X1, X2, X3, X4, X5, X6, splitcD_in_ggaaa(X2, X3, X7, X8, X6))
U33_gaa(X1, X2, X3, X4, X5, X6, splitcD_out_ggaaa(X2, X3, X7, X8, X6)) → U34_gaa(X1, X2, X3, X4, X5, X6, X7, mergesortcB_in_gaa(.(X1, X8), X9, X6))
U34_gaa(X1, X2, X3, X4, X5, X6, X7, mergesortcB_out_gaa(.(X1, X8), X9, X6)) → U35_gaa(X1, X2, X3, X4, X5, X6, X9, mergesortcE_in_gaa(X7, X10, X6))
mergesortcE_in_gaa([], [], X1) → mergesortcE_out_gaa([], [], X1)
mergesortcE_in_gaa(.(X1, []), .(X1, []), X2) → mergesortcE_out_gaa(.(X1, []), .(X1, []), X2)
mergesortcE_in_gaa(.(X1, .(X2, X3)), X4, .(X5, X6)) → U38_gaa(X1, X2, X3, X4, X5, X6, splitcD_in_ggaaa(X1, .(X2, X3), X7, X8, .(X5, X6)))
U38_gaa(X1, X2, X3, X4, X5, X6, splitcD_out_ggaaa(X1, .(X2, X3), X7, X8, .(X5, X6))) → U39_gaa(X1, X2, X3, X4, X5, X6, X8, mergesortcE_in_gaa(X7, X9, X6))
U39_gaa(X1, X2, X3, X4, X5, X6, X8, mergesortcE_out_gaa(X7, X9, X6)) → U40_gaa(X1, X2, X3, X4, X5, X6, X9, mergesortcE_in_gaa(X8, X10, X6))
U40_gaa(X1, X2, X3, X4, X5, X6, X9, mergesortcE_out_gaa(X8, X10, X6)) → U41_gaa(X1, X2, X3, X4, X5, X6, mergecC_in_ggaaa(X9, X10, X4, X5, X6))
mergecC_in_ggaaa([], X1, X1, X2, X3) → mergecC_out_ggaaa([], X1, X1, X2, X3)
mergecC_in_ggaaa(X1, [], X1, X2, X3) → mergecC_out_ggaaa(X1, [], X1, X2, X3)
mergecC_in_ggaaa(.(X1, X2), .(X3, X4), .(X1, X5), X6, X7) → U42_ggaaa(X1, X2, X3, X4, X5, X6, X7, qcF_in_ggggaa(X1, X3, X2, X4, X5, X7))
qcF_in_ggggaa(X1, X2, [], X3, .(X2, X3), X4) → U45_ggggaa(X1, X2, X3, X4, lecH_in_gg(X1, X2))
lecH_in_gg(s(X1), s(X2)) → U44_gg(X1, X2, lecH_in_gg(X1, X2))
lecH_in_gg(0, s(0)) → lecH_out_gg(0, s(0))
lecH_in_gg(0, 0) → lecH_out_gg(0, 0)
U44_gg(X1, X2, lecH_out_gg(X1, X2)) → lecH_out_gg(s(X1), s(X2))
U45_ggggaa(X1, X2, X3, X4, lecH_out_gg(X1, X2)) → qcF_out_ggggaa(X1, X2, [], X3, .(X2, X3), X4)
qcF_in_ggggaa(X1, X2, .(X3, X4), X5, .(X3, X6), .(X7, X8)) → U46_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, lecH_in_gg(X1, X2))
U46_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, lecH_out_gg(X1, X2)) → U47_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, qcF_in_ggggaa(X3, X2, X4, X5, X6, X8))
qcF_in_ggggaa(X1, X2, .(X3, X4), X5, .(X2, X6), .(X7, X8)) → U48_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, lecH_in_gg(X1, X2))
U48_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, lecH_out_gg(X1, X2)) → U49_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, qcG_in_ggggaa(X3, X2, X4, X5, X6, X8))
qcG_in_ggggaa(X1, X2, X3, [], .(X1, X3), X4) → U51_ggggaa(X1, X2, X3, X4, gtcI_in_gg(X1, X2))
gtcI_in_gg(s(X1), s(X2)) → U50_gg(X1, X2, gtcI_in_gg(X1, X2))
gtcI_in_gg(s(0), 0) → gtcI_out_gg(s(0), 0)
U50_gg(X1, X2, gtcI_out_gg(X1, X2)) → gtcI_out_gg(s(X1), s(X2))
U51_ggggaa(X1, X2, X3, X4, gtcI_out_gg(X1, X2)) → qcG_out_ggggaa(X1, X2, X3, [], .(X1, X3), X4)
qcG_in_ggggaa(X1, X2, X3, .(X4, X5), .(X1, X6), .(X7, X8)) → U52_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, gtcI_in_gg(X1, X2))
U52_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, gtcI_out_gg(X1, X2)) → U53_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, qcF_in_ggggaa(X1, X4, X3, X5, X6, X8))
U53_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, qcF_out_ggggaa(X1, X4, X3, X5, X6, X8)) → qcG_out_ggggaa(X1, X2, X3, .(X4, X5), .(X1, X6), .(X7, X8))
qcG_in_ggggaa(X1, X2, X3, .(X4, X5), .(X4, X6), .(X7, X8)) → U54_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, gtcI_in_gg(X1, X2))
U54_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, gtcI_out_gg(X1, X2)) → U55_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, qcG_in_ggggaa(X1, X4, X3, X5, X6, X8))
U55_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, qcG_out_ggggaa(X1, X4, X3, X5, X6, X8)) → qcG_out_ggggaa(X1, X2, X3, .(X4, X5), .(X4, X6), .(X7, X8))
U49_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, qcG_out_ggggaa(X3, X2, X4, X5, X6, X8)) → qcF_out_ggggaa(X1, X2, .(X3, X4), X5, .(X2, X6), .(X7, X8))
U47_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, qcF_out_ggggaa(X3, X2, X4, X5, X6, X8)) → qcF_out_ggggaa(X1, X2, .(X3, X4), X5, .(X3, X6), .(X7, X8))
U42_ggaaa(X1, X2, X3, X4, X5, X6, X7, qcF_out_ggggaa(X1, X3, X2, X4, X5, X7)) → mergecC_out_ggaaa(.(X1, X2), .(X3, X4), .(X1, X5), X6, X7)
mergecC_in_ggaaa(.(X1, X2), .(X3, X4), .(X3, X5), X6, X7) → U43_ggaaa(X1, X2, X3, X4, X5, X6, X7, qcG_in_ggggaa(X1, X3, X2, X4, X5, X7))
U43_ggaaa(X1, X2, X3, X4, X5, X6, X7, qcG_out_ggggaa(X1, X3, X2, X4, X5, X7)) → mergecC_out_ggaaa(.(X1, X2), .(X3, X4), .(X3, X5), X6, X7)
U41_gaa(X1, X2, X3, X4, X5, X6, mergecC_out_ggaaa(X9, X10, X4, X5, X6)) → mergesortcE_out_gaa(.(X1, .(X2, X3)), X4, .(X5, X6))
U35_gaa(X1, X2, X3, X4, X5, X6, X9, mergesortcE_out_gaa(X7, X10, X6)) → U36_gaa(X1, X2, X3, X4, X5, X6, mergecC_in_ggaaa(X9, X10, X4, X5, X6))
U36_gaa(X1, X2, X3, X4, X5, X6, mergecC_out_ggaaa(X9, X10, X4, X5, X6)) → mergesortcB_out_gaa(.(X1, .(X2, X3)), X4, .(X5, X6))

The argument filtering Pi contains the following mapping:
mergesortB_in_gaa(x1, x2, x3)  =  mergesortB_in_gaa(x1)
.(x1, x2)  =  .(x1, x2)
splitD_in_ggaaa(x1, x2, x3, x4, x5)  =  splitD_in_ggaaa(x1, x2)
splitA_in_gaaa(x1, x2, x3, x4)  =  splitA_in_gaaa(x1)
splitcD_in_ggaaa(x1, x2, x3, x4, x5)  =  splitcD_in_ggaaa(x1, x2)
U37_ggaaa(x1, x2, x3, x4, x5, x6, x7)  =  U37_ggaaa(x1, x2, x7)
splitcA_in_gaaa(x1, x2, x3, x4)  =  splitcA_in_gaaa(x1)
[]  =  []
splitcA_out_gaaa(x1, x2, x3, x4)  =  splitcA_out_gaaa(x1, x2, x3)
U32_gaaa(x1, x2, x3, x4, x5, x6, x7)  =  U32_gaaa(x1, x2, x7)
splitcD_out_ggaaa(x1, x2, x3, x4, x5)  =  splitcD_out_ggaaa(x1, x2, x3, x4)
mergesortcB_in_gaa(x1, x2, x3)  =  mergesortcB_in_gaa(x1)
mergesortcB_out_gaa(x1, x2, x3)  =  mergesortcB_out_gaa(x1, x2)
U33_gaa(x1, x2, x3, x4, x5, x6, x7)  =  U33_gaa(x1, x2, x3, x7)
U34_gaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  U34_gaa(x1, x2, x3, x7, x8)
U35_gaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  U35_gaa(x1, x2, x3, x7, x8)
mergesortcE_in_gaa(x1, x2, x3)  =  mergesortcE_in_gaa(x1)
mergesortcE_out_gaa(x1, x2, x3)  =  mergesortcE_out_gaa(x1, x2)
U38_gaa(x1, x2, x3, x4, x5, x6, x7)  =  U38_gaa(x1, x2, x3, x7)
U39_gaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  U39_gaa(x1, x2, x3, x7, x8)
U40_gaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  U40_gaa(x1, x2, x3, x7, x8)
U41_gaa(x1, x2, x3, x4, x5, x6, x7)  =  U41_gaa(x1, x2, x3, x7)
mergecC_in_ggaaa(x1, x2, x3, x4, x5)  =  mergecC_in_ggaaa(x1, x2)
mergecC_out_ggaaa(x1, x2, x3, x4, x5)  =  mergecC_out_ggaaa(x1, x2, x3)
U42_ggaaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  U42_ggaaa(x1, x2, x3, x4, x8)
qcF_in_ggggaa(x1, x2, x3, x4, x5, x6)  =  qcF_in_ggggaa(x1, x2, x3, x4)
U45_ggggaa(x1, x2, x3, x4, x5)  =  U45_ggggaa(x1, x2, x3, x5)
lecH_in_gg(x1, x2)  =  lecH_in_gg(x1, x2)
s(x1)  =  s(x1)
U44_gg(x1, x2, x3)  =  U44_gg(x1, x2, x3)
0  =  0
lecH_out_gg(x1, x2)  =  lecH_out_gg(x1, x2)
qcF_out_ggggaa(x1, x2, x3, x4, x5, x6)  =  qcF_out_ggggaa(x1, x2, x3, x4, x5)
U46_ggggaa(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U46_ggggaa(x1, x2, x3, x4, x5, x9)
U47_ggggaa(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U47_ggggaa(x1, x2, x3, x4, x5, x9)
U48_ggggaa(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U48_ggggaa(x1, x2, x3, x4, x5, x9)
U49_ggggaa(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U49_ggggaa(x1, x2, x3, x4, x5, x9)
qcG_in_ggggaa(x1, x2, x3, x4, x5, x6)  =  qcG_in_ggggaa(x1, x2, x3, x4)
U51_ggggaa(x1, x2, x3, x4, x5)  =  U51_ggggaa(x1, x2, x3, x5)
gtcI_in_gg(x1, x2)  =  gtcI_in_gg(x1, x2)
U50_gg(x1, x2, x3)  =  U50_gg(x1, x2, x3)
gtcI_out_gg(x1, x2)  =  gtcI_out_gg(x1, x2)
qcG_out_ggggaa(x1, x2, x3, x4, x5, x6)  =  qcG_out_ggggaa(x1, x2, x3, x4, x5)
U52_ggggaa(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U52_ggggaa(x1, x2, x3, x4, x5, x9)
U53_ggggaa(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U53_ggggaa(x1, x2, x3, x4, x5, x9)
U54_ggggaa(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U54_ggggaa(x1, x2, x3, x4, x5, x9)
U55_ggggaa(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U55_ggggaa(x1, x2, x3, x4, x5, x9)
U43_ggaaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  U43_ggaaa(x1, x2, x3, x4, x8)
U36_gaa(x1, x2, x3, x4, x5, x6, x7)  =  U36_gaa(x1, x2, x3, x7)
mergesortE_in_gaa(x1, x2, x3)  =  mergesortE_in_gaa(x1)
mergeC_in_ggaaa(x1, x2, x3, x4, x5)  =  mergeC_in_ggaaa(x1, x2)
pF_in_ggggaa(x1, x2, x3, x4, x5, x6)  =  pF_in_ggggaa(x1, x2, x3, x4)
leH_in_gg(x1, x2)  =  leH_in_gg(x1, x2)
pG_in_ggggaa(x1, x2, x3, x4, x5, x6)  =  pG_in_ggggaa(x1, x2, x3, x4)
gtI_in_gg(x1, x2)  =  gtI_in_gg(x1, x2)
MERGESORTB_IN_GAA(x1, x2, x3)  =  MERGESORTB_IN_GAA(x1)
U24_GAA(x1, x2, x3, x4, x5, x6, x7)  =  U24_GAA(x1, x2, x3, x7)
SPLITD_IN_GGAAA(x1, x2, x3, x4, x5)  =  SPLITD_IN_GGAAA(x1, x2)
U2_GGAAA(x1, x2, x3, x4, x5, x6, x7)  =  U2_GGAAA(x1, x2, x7)
SPLITA_IN_GAAA(x1, x2, x3, x4)  =  SPLITA_IN_GAAA(x1)
U1_GAAA(x1, x2, x3, x4, x5, x6, x7)  =  U1_GAAA(x1, x2, x7)
U25_GAA(x1, x2, x3, x4, x5, x6, x7)  =  U25_GAA(x1, x2, x3, x7)
U26_GAA(x1, x2, x3, x4, x5, x6, x7)  =  U26_GAA(x1, x2, x3, x7)
U27_GAA(x1, x2, x3, x4, x5, x6, x7, x8)  =  U27_GAA(x1, x2, x3, x7, x8)
U28_GAA(x1, x2, x3, x4, x5, x6, x7)  =  U28_GAA(x1, x2, x3, x7)
MERGESORTE_IN_GAA(x1, x2, x3)  =  MERGESORTE_IN_GAA(x1)
U3_GAA(x1, x2, x3, x4, x5, x6, x7)  =  U3_GAA(x1, x2, x3, x7)
U4_GAA(x1, x2, x3, x4, x5, x6, x7)  =  U4_GAA(x1, x2, x3, x7)
U5_GAA(x1, x2, x3, x4, x5, x6, x7)  =  U5_GAA(x1, x2, x3, x7)
U6_GAA(x1, x2, x3, x4, x5, x6, x7, x8)  =  U6_GAA(x1, x2, x3, x7, x8)
U7_GAA(x1, x2, x3, x4, x5, x6, x7)  =  U7_GAA(x1, x2, x3, x7)
U8_GAA(x1, x2, x3, x4, x5, x6, x7, x8)  =  U8_GAA(x1, x2, x3, x7, x8)
U9_GAA(x1, x2, x3, x4, x5, x6, x7)  =  U9_GAA(x1, x2, x3, x7)
MERGEC_IN_GGAAA(x1, x2, x3, x4, x5)  =  MERGEC_IN_GGAAA(x1, x2)
U10_GGAAA(x1, x2, x3, x4, x5, x6, x7, x8)  =  U10_GGAAA(x1, x2, x3, x4, x8)
PF_IN_GGGGAA(x1, x2, x3, x4, x5, x6)  =  PF_IN_GGGGAA(x1, x2, x3, x4)
U13_GGGGAA(x1, x2, x3, x4, x5, x6, x7)  =  U13_GGGGAA(x1, x2, x3, x4, x7)
LEH_IN_GG(x1, x2)  =  LEH_IN_GG(x1, x2)
U12_GG(x1, x2, x3)  =  U12_GG(x1, x2, x3)
U14_GGGGAA(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U14_GGGGAA(x1, x2, x3, x4, x5, x9)
U15_GGGGAA(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U15_GGGGAA(x1, x2, x3, x4, x5, x9)
U16_GGGGAA(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U16_GGGGAA(x1, x2, x3, x4, x5, x9)
U17_GGGGAA(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U17_GGGGAA(x1, x2, x3, x4, x5, x9)
PG_IN_GGGGAA(x1, x2, x3, x4, x5, x6)  =  PG_IN_GGGGAA(x1, x2, x3, x4)
U19_GGGGAA(x1, x2, x3, x4, x5, x6, x7)  =  U19_GGGGAA(x1, x2, x3, x4, x7)
GTI_IN_GG(x1, x2)  =  GTI_IN_GG(x1, x2)
U18_GG(x1, x2, x3)  =  U18_GG(x1, x2, x3)
U20_GGGGAA(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U20_GGGGAA(x1, x2, x3, x4, x5, x9)
U21_GGGGAA(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U21_GGGGAA(x1, x2, x3, x4, x5, x9)
U22_GGGGAA(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U22_GGGGAA(x1, x2, x3, x4, x5, x9)
U23_GGGGAA(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U23_GGGGAA(x1, x2, x3, x4, x5, x9)
U11_GGAAA(x1, x2, x3, x4, x5, x6, x7, x8)  =  U11_GGAAA(x1, x2, x3, x4, x8)
U29_GAA(x1, x2, x3, x4, x5, x6, x7, x8)  =  U29_GAA(x1, x2, x3, x7, x8)
U30_GAA(x1, x2, x3, x4, x5, x6, x7)  =  U30_GAA(x1, x2, x3, x7)

We have to consider all (P,R,Pi)-chains

Infinitary Constructor Rewriting Termination of PiDP implies Termination of TRIPLES

(4) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

MERGESORTB_IN_GAA(.(X1, .(X2, X3)), X4, .(X5, X6)) → U24_GAA(X1, X2, X3, X4, X5, X6, splitD_in_ggaaa(X2, X3, X7, X8, X6))
MERGESORTB_IN_GAA(.(X1, .(X2, X3)), X4, .(X5, X6)) → SPLITD_IN_GGAAA(X2, X3, X7, X8, X6)
SPLITD_IN_GGAAA(X1, X2, .(X1, X3), X4, .(X5, X6)) → U2_GGAAA(X1, X2, X3, X4, X5, X6, splitA_in_gaaa(X2, X4, X3, X6))
SPLITD_IN_GGAAA(X1, X2, .(X1, X3), X4, .(X5, X6)) → SPLITA_IN_GAAA(X2, X4, X3, X6)
SPLITA_IN_GAAA(.(X1, X2), .(X1, X3), X4, .(X5, X6)) → U1_GAAA(X1, X2, X3, X4, X5, X6, splitA_in_gaaa(X2, X4, X3, X6))
SPLITA_IN_GAAA(.(X1, X2), .(X1, X3), X4, .(X5, X6)) → SPLITA_IN_GAAA(X2, X4, X3, X6)
MERGESORTB_IN_GAA(.(X1, .(X2, X3)), X4, .(X5, X6)) → U25_GAA(X1, X2, X3, X4, X5, X6, splitcD_in_ggaaa(X2, X3, X7, X8, X6))
U25_GAA(X1, X2, X3, X4, X5, X6, splitcD_out_ggaaa(X2, X3, X7, X8, X6)) → U26_GAA(X1, X2, X3, X4, X5, X6, mergesortB_in_gaa(.(X1, X8), X9, X6))
U25_GAA(X1, X2, X3, X4, X5, X6, splitcD_out_ggaaa(X2, X3, X7, X8, X6)) → MERGESORTB_IN_GAA(.(X1, X8), X9, X6)
U25_GAA(X1, X2, X3, X4, X5, X6, splitcD_out_ggaaa(X2, X3, X7, X8, X6)) → U27_GAA(X1, X2, X3, X4, X5, X6, X7, mergesortcB_in_gaa(.(X1, X8), X9, X6))
U27_GAA(X1, X2, X3, X4, X5, X6, X7, mergesortcB_out_gaa(.(X1, X8), X9, X6)) → U28_GAA(X1, X2, X3, X4, X5, X6, mergesortE_in_gaa(X7, X10, X6))
U27_GAA(X1, X2, X3, X4, X5, X6, X7, mergesortcB_out_gaa(.(X1, X8), X9, X6)) → MERGESORTE_IN_GAA(X7, X10, X6)
MERGESORTE_IN_GAA(.(X1, .(X2, X3)), X4, .(X5, X6)) → U3_GAA(X1, X2, X3, X4, X5, X6, splitD_in_ggaaa(X1, .(X2, X3), X7, X8, .(X5, X6)))
MERGESORTE_IN_GAA(.(X1, .(X2, X3)), X4, .(X5, X6)) → SPLITD_IN_GGAAA(X1, .(X2, X3), X7, X8, .(X5, X6))
MERGESORTE_IN_GAA(.(X1, .(X2, X3)), X4, .(X5, X6)) → U4_GAA(X1, X2, X3, X4, X5, X6, splitcD_in_ggaaa(X1, .(X2, X3), X7, X8, .(X5, X6)))
U4_GAA(X1, X2, X3, X4, X5, X6, splitcD_out_ggaaa(X1, .(X2, X3), X7, X8, .(X5, X6))) → U5_GAA(X1, X2, X3, X4, X5, X6, mergesortE_in_gaa(X7, X9, X6))
U4_GAA(X1, X2, X3, X4, X5, X6, splitcD_out_ggaaa(X1, .(X2, X3), X7, X8, .(X5, X6))) → MERGESORTE_IN_GAA(X7, X9, X6)
U4_GAA(X1, X2, X3, X4, X5, X6, splitcD_out_ggaaa(X1, .(X2, X3), X7, X8, .(X5, X6))) → U6_GAA(X1, X2, X3, X4, X5, X6, X8, mergesortcE_in_gaa(X7, X9, X6))
U6_GAA(X1, X2, X3, X4, X5, X6, X8, mergesortcE_out_gaa(X7, X9, X6)) → U7_GAA(X1, X2, X3, X4, X5, X6, mergesortE_in_gaa(X8, X10, X6))
U6_GAA(X1, X2, X3, X4, X5, X6, X8, mergesortcE_out_gaa(X7, X9, X6)) → MERGESORTE_IN_GAA(X8, X10, X6)
U6_GAA(X1, X2, X3, X4, X5, X6, X8, mergesortcE_out_gaa(X7, X9, X6)) → U8_GAA(X1, X2, X3, X4, X5, X6, X9, mergesortcE_in_gaa(X8, X10, X6))
U8_GAA(X1, X2, X3, X4, X5, X6, X9, mergesortcE_out_gaa(X8, X10, X6)) → U9_GAA(X1, X2, X3, X4, X5, X6, mergeC_in_ggaaa(X9, X10, X4, X5, X6))
U8_GAA(X1, X2, X3, X4, X5, X6, X9, mergesortcE_out_gaa(X8, X10, X6)) → MERGEC_IN_GGAAA(X9, X10, X4, X5, X6)
MERGEC_IN_GGAAA(.(X1, X2), .(X3, X4), .(X1, X5), X6, X7) → U10_GGAAA(X1, X2, X3, X4, X5, X6, X7, pF_in_ggggaa(X1, X3, X2, X4, X5, X7))
MERGEC_IN_GGAAA(.(X1, X2), .(X3, X4), .(X1, X5), X6, X7) → PF_IN_GGGGAA(X1, X3, X2, X4, X5, X7)
PF_IN_GGGGAA(X1, X2, X3, X4, X5, X6) → U13_GGGGAA(X1, X2, X3, X4, X5, X6, leH_in_gg(X1, X2))
PF_IN_GGGGAA(X1, X2, X3, X4, X5, X6) → LEH_IN_GG(X1, X2)
LEH_IN_GG(s(X1), s(X2)) → U12_GG(X1, X2, leH_in_gg(X1, X2))
LEH_IN_GG(s(X1), s(X2)) → LEH_IN_GG(X1, X2)
PF_IN_GGGGAA(X1, X2, .(X3, X4), X5, .(X3, X6), .(X7, X8)) → U14_GGGGAA(X1, X2, X3, X4, X5, X6, X7, X8, lecH_in_gg(X1, X2))
U14_GGGGAA(X1, X2, X3, X4, X5, X6, X7, X8, lecH_out_gg(X1, X2)) → U15_GGGGAA(X1, X2, X3, X4, X5, X6, X7, X8, pF_in_ggggaa(X3, X2, X4, X5, X6, X8))
U14_GGGGAA(X1, X2, X3, X4, X5, X6, X7, X8, lecH_out_gg(X1, X2)) → PF_IN_GGGGAA(X3, X2, X4, X5, X6, X8)
PF_IN_GGGGAA(X1, X2, .(X3, X4), X5, .(X2, X6), .(X7, X8)) → U16_GGGGAA(X1, X2, X3, X4, X5, X6, X7, X8, lecH_in_gg(X1, X2))
U16_GGGGAA(X1, X2, X3, X4, X5, X6, X7, X8, lecH_out_gg(X1, X2)) → U17_GGGGAA(X1, X2, X3, X4, X5, X6, X7, X8, pG_in_ggggaa(X3, X2, X4, X5, X6, X8))
U16_GGGGAA(X1, X2, X3, X4, X5, X6, X7, X8, lecH_out_gg(X1, X2)) → PG_IN_GGGGAA(X3, X2, X4, X5, X6, X8)
PG_IN_GGGGAA(X1, X2, X3, X4, X5, X6) → U19_GGGGAA(X1, X2, X3, X4, X5, X6, gtI_in_gg(X1, X2))
PG_IN_GGGGAA(X1, X2, X3, X4, X5, X6) → GTI_IN_GG(X1, X2)
GTI_IN_GG(s(X1), s(X2)) → U18_GG(X1, X2, gtI_in_gg(X1, X2))
GTI_IN_GG(s(X1), s(X2)) → GTI_IN_GG(X1, X2)
PG_IN_GGGGAA(X1, X2, X3, .(X4, X5), .(X1, X6), .(X7, X8)) → U20_GGGGAA(X1, X2, X3, X4, X5, X6, X7, X8, gtcI_in_gg(X1, X2))
U20_GGGGAA(X1, X2, X3, X4, X5, X6, X7, X8, gtcI_out_gg(X1, X2)) → U21_GGGGAA(X1, X2, X3, X4, X5, X6, X7, X8, pF_in_ggggaa(X1, X4, X3, X5, X6, X8))
U20_GGGGAA(X1, X2, X3, X4, X5, X6, X7, X8, gtcI_out_gg(X1, X2)) → PF_IN_GGGGAA(X1, X4, X3, X5, X6, X8)
PG_IN_GGGGAA(X1, X2, X3, .(X4, X5), .(X4, X6), .(X7, X8)) → U22_GGGGAA(X1, X2, X3, X4, X5, X6, X7, X8, gtcI_in_gg(X1, X2))
U22_GGGGAA(X1, X2, X3, X4, X5, X6, X7, X8, gtcI_out_gg(X1, X2)) → U23_GGGGAA(X1, X2, X3, X4, X5, X6, X7, X8, pG_in_ggggaa(X1, X4, X3, X5, X6, X8))
U22_GGGGAA(X1, X2, X3, X4, X5, X6, X7, X8, gtcI_out_gg(X1, X2)) → PG_IN_GGGGAA(X1, X4, X3, X5, X6, X8)
MERGEC_IN_GGAAA(.(X1, X2), .(X3, X4), .(X3, X5), X6, X7) → U11_GGAAA(X1, X2, X3, X4, X5, X6, X7, pG_in_ggggaa(X1, X3, X2, X4, X5, X7))
MERGEC_IN_GGAAA(.(X1, X2), .(X3, X4), .(X3, X5), X6, X7) → PG_IN_GGGGAA(X1, X3, X2, X4, X5, X7)
U27_GAA(X1, X2, X3, X4, X5, X6, X7, mergesortcB_out_gaa(.(X1, X8), X9, X6)) → U29_GAA(X1, X2, X3, X4, X5, X6, X9, mergesortcE_in_gaa(X7, X10, X6))
U29_GAA(X1, X2, X3, X4, X5, X6, X9, mergesortcE_out_gaa(X7, X10, X6)) → U30_GAA(X1, X2, X3, X4, X5, X6, mergeC_in_ggaaa(X9, X10, X4, X5, X6))
U29_GAA(X1, X2, X3, X4, X5, X6, X9, mergesortcE_out_gaa(X7, X10, X6)) → MERGEC_IN_GGAAA(X9, X10, X4, X5, X6)

The TRS R consists of the following rules:

splitcD_in_ggaaa(X1, X2, .(X1, X3), X4, .(X5, X6)) → U37_ggaaa(X1, X2, X3, X4, X5, X6, splitcA_in_gaaa(X2, X4, X3, X6))
splitcA_in_gaaa([], [], [], X1) → splitcA_out_gaaa([], [], [], X1)
splitcA_in_gaaa(.(X1, X2), .(X1, X3), X4, .(X5, X6)) → U32_gaaa(X1, X2, X3, X4, X5, X6, splitcA_in_gaaa(X2, X4, X3, X6))
U32_gaaa(X1, X2, X3, X4, X5, X6, splitcA_out_gaaa(X2, X4, X3, X6)) → splitcA_out_gaaa(.(X1, X2), .(X1, X3), X4, .(X5, X6))
U37_ggaaa(X1, X2, X3, X4, X5, X6, splitcA_out_gaaa(X2, X4, X3, X6)) → splitcD_out_ggaaa(X1, X2, .(X1, X3), X4, .(X5, X6))
mergesortcB_in_gaa([], [], X1) → mergesortcB_out_gaa([], [], X1)
mergesortcB_in_gaa(.(X1, []), .(X1, []), X2) → mergesortcB_out_gaa(.(X1, []), .(X1, []), X2)
mergesortcB_in_gaa(.(X1, .(X2, X3)), X4, .(X5, X6)) → U33_gaa(X1, X2, X3, X4, X5, X6, splitcD_in_ggaaa(X2, X3, X7, X8, X6))
U33_gaa(X1, X2, X3, X4, X5, X6, splitcD_out_ggaaa(X2, X3, X7, X8, X6)) → U34_gaa(X1, X2, X3, X4, X5, X6, X7, mergesortcB_in_gaa(.(X1, X8), X9, X6))
U34_gaa(X1, X2, X3, X4, X5, X6, X7, mergesortcB_out_gaa(.(X1, X8), X9, X6)) → U35_gaa(X1, X2, X3, X4, X5, X6, X9, mergesortcE_in_gaa(X7, X10, X6))
mergesortcE_in_gaa([], [], X1) → mergesortcE_out_gaa([], [], X1)
mergesortcE_in_gaa(.(X1, []), .(X1, []), X2) → mergesortcE_out_gaa(.(X1, []), .(X1, []), X2)
mergesortcE_in_gaa(.(X1, .(X2, X3)), X4, .(X5, X6)) → U38_gaa(X1, X2, X3, X4, X5, X6, splitcD_in_ggaaa(X1, .(X2, X3), X7, X8, .(X5, X6)))
U38_gaa(X1, X2, X3, X4, X5, X6, splitcD_out_ggaaa(X1, .(X2, X3), X7, X8, .(X5, X6))) → U39_gaa(X1, X2, X3, X4, X5, X6, X8, mergesortcE_in_gaa(X7, X9, X6))
U39_gaa(X1, X2, X3, X4, X5, X6, X8, mergesortcE_out_gaa(X7, X9, X6)) → U40_gaa(X1, X2, X3, X4, X5, X6, X9, mergesortcE_in_gaa(X8, X10, X6))
U40_gaa(X1, X2, X3, X4, X5, X6, X9, mergesortcE_out_gaa(X8, X10, X6)) → U41_gaa(X1, X2, X3, X4, X5, X6, mergecC_in_ggaaa(X9, X10, X4, X5, X6))
mergecC_in_ggaaa([], X1, X1, X2, X3) → mergecC_out_ggaaa([], X1, X1, X2, X3)
mergecC_in_ggaaa(X1, [], X1, X2, X3) → mergecC_out_ggaaa(X1, [], X1, X2, X3)
mergecC_in_ggaaa(.(X1, X2), .(X3, X4), .(X1, X5), X6, X7) → U42_ggaaa(X1, X2, X3, X4, X5, X6, X7, qcF_in_ggggaa(X1, X3, X2, X4, X5, X7))
qcF_in_ggggaa(X1, X2, [], X3, .(X2, X3), X4) → U45_ggggaa(X1, X2, X3, X4, lecH_in_gg(X1, X2))
lecH_in_gg(s(X1), s(X2)) → U44_gg(X1, X2, lecH_in_gg(X1, X2))
lecH_in_gg(0, s(0)) → lecH_out_gg(0, s(0))
lecH_in_gg(0, 0) → lecH_out_gg(0, 0)
U44_gg(X1, X2, lecH_out_gg(X1, X2)) → lecH_out_gg(s(X1), s(X2))
U45_ggggaa(X1, X2, X3, X4, lecH_out_gg(X1, X2)) → qcF_out_ggggaa(X1, X2, [], X3, .(X2, X3), X4)
qcF_in_ggggaa(X1, X2, .(X3, X4), X5, .(X3, X6), .(X7, X8)) → U46_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, lecH_in_gg(X1, X2))
U46_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, lecH_out_gg(X1, X2)) → U47_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, qcF_in_ggggaa(X3, X2, X4, X5, X6, X8))
qcF_in_ggggaa(X1, X2, .(X3, X4), X5, .(X2, X6), .(X7, X8)) → U48_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, lecH_in_gg(X1, X2))
U48_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, lecH_out_gg(X1, X2)) → U49_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, qcG_in_ggggaa(X3, X2, X4, X5, X6, X8))
qcG_in_ggggaa(X1, X2, X3, [], .(X1, X3), X4) → U51_ggggaa(X1, X2, X3, X4, gtcI_in_gg(X1, X2))
gtcI_in_gg(s(X1), s(X2)) → U50_gg(X1, X2, gtcI_in_gg(X1, X2))
gtcI_in_gg(s(0), 0) → gtcI_out_gg(s(0), 0)
U50_gg(X1, X2, gtcI_out_gg(X1, X2)) → gtcI_out_gg(s(X1), s(X2))
U51_ggggaa(X1, X2, X3, X4, gtcI_out_gg(X1, X2)) → qcG_out_ggggaa(X1, X2, X3, [], .(X1, X3), X4)
qcG_in_ggggaa(X1, X2, X3, .(X4, X5), .(X1, X6), .(X7, X8)) → U52_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, gtcI_in_gg(X1, X2))
U52_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, gtcI_out_gg(X1, X2)) → U53_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, qcF_in_ggggaa(X1, X4, X3, X5, X6, X8))
U53_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, qcF_out_ggggaa(X1, X4, X3, X5, X6, X8)) → qcG_out_ggggaa(X1, X2, X3, .(X4, X5), .(X1, X6), .(X7, X8))
qcG_in_ggggaa(X1, X2, X3, .(X4, X5), .(X4, X6), .(X7, X8)) → U54_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, gtcI_in_gg(X1, X2))
U54_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, gtcI_out_gg(X1, X2)) → U55_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, qcG_in_ggggaa(X1, X4, X3, X5, X6, X8))
U55_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, qcG_out_ggggaa(X1, X4, X3, X5, X6, X8)) → qcG_out_ggggaa(X1, X2, X3, .(X4, X5), .(X4, X6), .(X7, X8))
U49_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, qcG_out_ggggaa(X3, X2, X4, X5, X6, X8)) → qcF_out_ggggaa(X1, X2, .(X3, X4), X5, .(X2, X6), .(X7, X8))
U47_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, qcF_out_ggggaa(X3, X2, X4, X5, X6, X8)) → qcF_out_ggggaa(X1, X2, .(X3, X4), X5, .(X3, X6), .(X7, X8))
U42_ggaaa(X1, X2, X3, X4, X5, X6, X7, qcF_out_ggggaa(X1, X3, X2, X4, X5, X7)) → mergecC_out_ggaaa(.(X1, X2), .(X3, X4), .(X1, X5), X6, X7)
mergecC_in_ggaaa(.(X1, X2), .(X3, X4), .(X3, X5), X6, X7) → U43_ggaaa(X1, X2, X3, X4, X5, X6, X7, qcG_in_ggggaa(X1, X3, X2, X4, X5, X7))
U43_ggaaa(X1, X2, X3, X4, X5, X6, X7, qcG_out_ggggaa(X1, X3, X2, X4, X5, X7)) → mergecC_out_ggaaa(.(X1, X2), .(X3, X4), .(X3, X5), X6, X7)
U41_gaa(X1, X2, X3, X4, X5, X6, mergecC_out_ggaaa(X9, X10, X4, X5, X6)) → mergesortcE_out_gaa(.(X1, .(X2, X3)), X4, .(X5, X6))
U35_gaa(X1, X2, X3, X4, X5, X6, X9, mergesortcE_out_gaa(X7, X10, X6)) → U36_gaa(X1, X2, X3, X4, X5, X6, mergecC_in_ggaaa(X9, X10, X4, X5, X6))
U36_gaa(X1, X2, X3, X4, X5, X6, mergecC_out_ggaaa(X9, X10, X4, X5, X6)) → mergesortcB_out_gaa(.(X1, .(X2, X3)), X4, .(X5, X6))

The argument filtering Pi contains the following mapping:
mergesortB_in_gaa(x1, x2, x3)  =  mergesortB_in_gaa(x1)
.(x1, x2)  =  .(x1, x2)
splitD_in_ggaaa(x1, x2, x3, x4, x5)  =  splitD_in_ggaaa(x1, x2)
splitA_in_gaaa(x1, x2, x3, x4)  =  splitA_in_gaaa(x1)
splitcD_in_ggaaa(x1, x2, x3, x4, x5)  =  splitcD_in_ggaaa(x1, x2)
U37_ggaaa(x1, x2, x3, x4, x5, x6, x7)  =  U37_ggaaa(x1, x2, x7)
splitcA_in_gaaa(x1, x2, x3, x4)  =  splitcA_in_gaaa(x1)
[]  =  []
splitcA_out_gaaa(x1, x2, x3, x4)  =  splitcA_out_gaaa(x1, x2, x3)
U32_gaaa(x1, x2, x3, x4, x5, x6, x7)  =  U32_gaaa(x1, x2, x7)
splitcD_out_ggaaa(x1, x2, x3, x4, x5)  =  splitcD_out_ggaaa(x1, x2, x3, x4)
mergesortcB_in_gaa(x1, x2, x3)  =  mergesortcB_in_gaa(x1)
mergesortcB_out_gaa(x1, x2, x3)  =  mergesortcB_out_gaa(x1, x2)
U33_gaa(x1, x2, x3, x4, x5, x6, x7)  =  U33_gaa(x1, x2, x3, x7)
U34_gaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  U34_gaa(x1, x2, x3, x7, x8)
U35_gaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  U35_gaa(x1, x2, x3, x7, x8)
mergesortcE_in_gaa(x1, x2, x3)  =  mergesortcE_in_gaa(x1)
mergesortcE_out_gaa(x1, x2, x3)  =  mergesortcE_out_gaa(x1, x2)
U38_gaa(x1, x2, x3, x4, x5, x6, x7)  =  U38_gaa(x1, x2, x3, x7)
U39_gaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  U39_gaa(x1, x2, x3, x7, x8)
U40_gaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  U40_gaa(x1, x2, x3, x7, x8)
U41_gaa(x1, x2, x3, x4, x5, x6, x7)  =  U41_gaa(x1, x2, x3, x7)
mergecC_in_ggaaa(x1, x2, x3, x4, x5)  =  mergecC_in_ggaaa(x1, x2)
mergecC_out_ggaaa(x1, x2, x3, x4, x5)  =  mergecC_out_ggaaa(x1, x2, x3)
U42_ggaaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  U42_ggaaa(x1, x2, x3, x4, x8)
qcF_in_ggggaa(x1, x2, x3, x4, x5, x6)  =  qcF_in_ggggaa(x1, x2, x3, x4)
U45_ggggaa(x1, x2, x3, x4, x5)  =  U45_ggggaa(x1, x2, x3, x5)
lecH_in_gg(x1, x2)  =  lecH_in_gg(x1, x2)
s(x1)  =  s(x1)
U44_gg(x1, x2, x3)  =  U44_gg(x1, x2, x3)
0  =  0
lecH_out_gg(x1, x2)  =  lecH_out_gg(x1, x2)
qcF_out_ggggaa(x1, x2, x3, x4, x5, x6)  =  qcF_out_ggggaa(x1, x2, x3, x4, x5)
U46_ggggaa(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U46_ggggaa(x1, x2, x3, x4, x5, x9)
U47_ggggaa(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U47_ggggaa(x1, x2, x3, x4, x5, x9)
U48_ggggaa(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U48_ggggaa(x1, x2, x3, x4, x5, x9)
U49_ggggaa(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U49_ggggaa(x1, x2, x3, x4, x5, x9)
qcG_in_ggggaa(x1, x2, x3, x4, x5, x6)  =  qcG_in_ggggaa(x1, x2, x3, x4)
U51_ggggaa(x1, x2, x3, x4, x5)  =  U51_ggggaa(x1, x2, x3, x5)
gtcI_in_gg(x1, x2)  =  gtcI_in_gg(x1, x2)
U50_gg(x1, x2, x3)  =  U50_gg(x1, x2, x3)
gtcI_out_gg(x1, x2)  =  gtcI_out_gg(x1, x2)
qcG_out_ggggaa(x1, x2, x3, x4, x5, x6)  =  qcG_out_ggggaa(x1, x2, x3, x4, x5)
U52_ggggaa(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U52_ggggaa(x1, x2, x3, x4, x5, x9)
U53_ggggaa(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U53_ggggaa(x1, x2, x3, x4, x5, x9)
U54_ggggaa(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U54_ggggaa(x1, x2, x3, x4, x5, x9)
U55_ggggaa(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U55_ggggaa(x1, x2, x3, x4, x5, x9)
U43_ggaaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  U43_ggaaa(x1, x2, x3, x4, x8)
U36_gaa(x1, x2, x3, x4, x5, x6, x7)  =  U36_gaa(x1, x2, x3, x7)
mergesortE_in_gaa(x1, x2, x3)  =  mergesortE_in_gaa(x1)
mergeC_in_ggaaa(x1, x2, x3, x4, x5)  =  mergeC_in_ggaaa(x1, x2)
pF_in_ggggaa(x1, x2, x3, x4, x5, x6)  =  pF_in_ggggaa(x1, x2, x3, x4)
leH_in_gg(x1, x2)  =  leH_in_gg(x1, x2)
pG_in_ggggaa(x1, x2, x3, x4, x5, x6)  =  pG_in_ggggaa(x1, x2, x3, x4)
gtI_in_gg(x1, x2)  =  gtI_in_gg(x1, x2)
MERGESORTB_IN_GAA(x1, x2, x3)  =  MERGESORTB_IN_GAA(x1)
U24_GAA(x1, x2, x3, x4, x5, x6, x7)  =  U24_GAA(x1, x2, x3, x7)
SPLITD_IN_GGAAA(x1, x2, x3, x4, x5)  =  SPLITD_IN_GGAAA(x1, x2)
U2_GGAAA(x1, x2, x3, x4, x5, x6, x7)  =  U2_GGAAA(x1, x2, x7)
SPLITA_IN_GAAA(x1, x2, x3, x4)  =  SPLITA_IN_GAAA(x1)
U1_GAAA(x1, x2, x3, x4, x5, x6, x7)  =  U1_GAAA(x1, x2, x7)
U25_GAA(x1, x2, x3, x4, x5, x6, x7)  =  U25_GAA(x1, x2, x3, x7)
U26_GAA(x1, x2, x3, x4, x5, x6, x7)  =  U26_GAA(x1, x2, x3, x7)
U27_GAA(x1, x2, x3, x4, x5, x6, x7, x8)  =  U27_GAA(x1, x2, x3, x7, x8)
U28_GAA(x1, x2, x3, x4, x5, x6, x7)  =  U28_GAA(x1, x2, x3, x7)
MERGESORTE_IN_GAA(x1, x2, x3)  =  MERGESORTE_IN_GAA(x1)
U3_GAA(x1, x2, x3, x4, x5, x6, x7)  =  U3_GAA(x1, x2, x3, x7)
U4_GAA(x1, x2, x3, x4, x5, x6, x7)  =  U4_GAA(x1, x2, x3, x7)
U5_GAA(x1, x2, x3, x4, x5, x6, x7)  =  U5_GAA(x1, x2, x3, x7)
U6_GAA(x1, x2, x3, x4, x5, x6, x7, x8)  =  U6_GAA(x1, x2, x3, x7, x8)
U7_GAA(x1, x2, x3, x4, x5, x6, x7)  =  U7_GAA(x1, x2, x3, x7)
U8_GAA(x1, x2, x3, x4, x5, x6, x7, x8)  =  U8_GAA(x1, x2, x3, x7, x8)
U9_GAA(x1, x2, x3, x4, x5, x6, x7)  =  U9_GAA(x1, x2, x3, x7)
MERGEC_IN_GGAAA(x1, x2, x3, x4, x5)  =  MERGEC_IN_GGAAA(x1, x2)
U10_GGAAA(x1, x2, x3, x4, x5, x6, x7, x8)  =  U10_GGAAA(x1, x2, x3, x4, x8)
PF_IN_GGGGAA(x1, x2, x3, x4, x5, x6)  =  PF_IN_GGGGAA(x1, x2, x3, x4)
U13_GGGGAA(x1, x2, x3, x4, x5, x6, x7)  =  U13_GGGGAA(x1, x2, x3, x4, x7)
LEH_IN_GG(x1, x2)  =  LEH_IN_GG(x1, x2)
U12_GG(x1, x2, x3)  =  U12_GG(x1, x2, x3)
U14_GGGGAA(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U14_GGGGAA(x1, x2, x3, x4, x5, x9)
U15_GGGGAA(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U15_GGGGAA(x1, x2, x3, x4, x5, x9)
U16_GGGGAA(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U16_GGGGAA(x1, x2, x3, x4, x5, x9)
U17_GGGGAA(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U17_GGGGAA(x1, x2, x3, x4, x5, x9)
PG_IN_GGGGAA(x1, x2, x3, x4, x5, x6)  =  PG_IN_GGGGAA(x1, x2, x3, x4)
U19_GGGGAA(x1, x2, x3, x4, x5, x6, x7)  =  U19_GGGGAA(x1, x2, x3, x4, x7)
GTI_IN_GG(x1, x2)  =  GTI_IN_GG(x1, x2)
U18_GG(x1, x2, x3)  =  U18_GG(x1, x2, x3)
U20_GGGGAA(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U20_GGGGAA(x1, x2, x3, x4, x5, x9)
U21_GGGGAA(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U21_GGGGAA(x1, x2, x3, x4, x5, x9)
U22_GGGGAA(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U22_GGGGAA(x1, x2, x3, x4, x5, x9)
U23_GGGGAA(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U23_GGGGAA(x1, x2, x3, x4, x5, x9)
U11_GGAAA(x1, x2, x3, x4, x5, x6, x7, x8)  =  U11_GGAAA(x1, x2, x3, x4, x8)
U29_GAA(x1, x2, x3, x4, x5, x6, x7, x8)  =  U29_GAA(x1, x2, x3, x7, x8)
U30_GAA(x1, x2, x3, x4, x5, x6, x7)  =  U30_GAA(x1, x2, x3, x7)

We have to consider all (P,R,Pi)-chains

(5) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LOPSTR] contains 6 SCCs with 33 less nodes.

(6) Complex Obligation (AND)

(7) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

GTI_IN_GG(s(X1), s(X2)) → GTI_IN_GG(X1, X2)

The TRS R consists of the following rules:

splitcD_in_ggaaa(X1, X2, .(X1, X3), X4, .(X5, X6)) → U37_ggaaa(X1, X2, X3, X4, X5, X6, splitcA_in_gaaa(X2, X4, X3, X6))
splitcA_in_gaaa([], [], [], X1) → splitcA_out_gaaa([], [], [], X1)
splitcA_in_gaaa(.(X1, X2), .(X1, X3), X4, .(X5, X6)) → U32_gaaa(X1, X2, X3, X4, X5, X6, splitcA_in_gaaa(X2, X4, X3, X6))
U32_gaaa(X1, X2, X3, X4, X5, X6, splitcA_out_gaaa(X2, X4, X3, X6)) → splitcA_out_gaaa(.(X1, X2), .(X1, X3), X4, .(X5, X6))
U37_ggaaa(X1, X2, X3, X4, X5, X6, splitcA_out_gaaa(X2, X4, X3, X6)) → splitcD_out_ggaaa(X1, X2, .(X1, X3), X4, .(X5, X6))
mergesortcB_in_gaa([], [], X1) → mergesortcB_out_gaa([], [], X1)
mergesortcB_in_gaa(.(X1, []), .(X1, []), X2) → mergesortcB_out_gaa(.(X1, []), .(X1, []), X2)
mergesortcB_in_gaa(.(X1, .(X2, X3)), X4, .(X5, X6)) → U33_gaa(X1, X2, X3, X4, X5, X6, splitcD_in_ggaaa(X2, X3, X7, X8, X6))
U33_gaa(X1, X2, X3, X4, X5, X6, splitcD_out_ggaaa(X2, X3, X7, X8, X6)) → U34_gaa(X1, X2, X3, X4, X5, X6, X7, mergesortcB_in_gaa(.(X1, X8), X9, X6))
U34_gaa(X1, X2, X3, X4, X5, X6, X7, mergesortcB_out_gaa(.(X1, X8), X9, X6)) → U35_gaa(X1, X2, X3, X4, X5, X6, X9, mergesortcE_in_gaa(X7, X10, X6))
mergesortcE_in_gaa([], [], X1) → mergesortcE_out_gaa([], [], X1)
mergesortcE_in_gaa(.(X1, []), .(X1, []), X2) → mergesortcE_out_gaa(.(X1, []), .(X1, []), X2)
mergesortcE_in_gaa(.(X1, .(X2, X3)), X4, .(X5, X6)) → U38_gaa(X1, X2, X3, X4, X5, X6, splitcD_in_ggaaa(X1, .(X2, X3), X7, X8, .(X5, X6)))
U38_gaa(X1, X2, X3, X4, X5, X6, splitcD_out_ggaaa(X1, .(X2, X3), X7, X8, .(X5, X6))) → U39_gaa(X1, X2, X3, X4, X5, X6, X8, mergesortcE_in_gaa(X7, X9, X6))
U39_gaa(X1, X2, X3, X4, X5, X6, X8, mergesortcE_out_gaa(X7, X9, X6)) → U40_gaa(X1, X2, X3, X4, X5, X6, X9, mergesortcE_in_gaa(X8, X10, X6))
U40_gaa(X1, X2, X3, X4, X5, X6, X9, mergesortcE_out_gaa(X8, X10, X6)) → U41_gaa(X1, X2, X3, X4, X5, X6, mergecC_in_ggaaa(X9, X10, X4, X5, X6))
mergecC_in_ggaaa([], X1, X1, X2, X3) → mergecC_out_ggaaa([], X1, X1, X2, X3)
mergecC_in_ggaaa(X1, [], X1, X2, X3) → mergecC_out_ggaaa(X1, [], X1, X2, X3)
mergecC_in_ggaaa(.(X1, X2), .(X3, X4), .(X1, X5), X6, X7) → U42_ggaaa(X1, X2, X3, X4, X5, X6, X7, qcF_in_ggggaa(X1, X3, X2, X4, X5, X7))
qcF_in_ggggaa(X1, X2, [], X3, .(X2, X3), X4) → U45_ggggaa(X1, X2, X3, X4, lecH_in_gg(X1, X2))
lecH_in_gg(s(X1), s(X2)) → U44_gg(X1, X2, lecH_in_gg(X1, X2))
lecH_in_gg(0, s(0)) → lecH_out_gg(0, s(0))
lecH_in_gg(0, 0) → lecH_out_gg(0, 0)
U44_gg(X1, X2, lecH_out_gg(X1, X2)) → lecH_out_gg(s(X1), s(X2))
U45_ggggaa(X1, X2, X3, X4, lecH_out_gg(X1, X2)) → qcF_out_ggggaa(X1, X2, [], X3, .(X2, X3), X4)
qcF_in_ggggaa(X1, X2, .(X3, X4), X5, .(X3, X6), .(X7, X8)) → U46_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, lecH_in_gg(X1, X2))
U46_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, lecH_out_gg(X1, X2)) → U47_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, qcF_in_ggggaa(X3, X2, X4, X5, X6, X8))
qcF_in_ggggaa(X1, X2, .(X3, X4), X5, .(X2, X6), .(X7, X8)) → U48_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, lecH_in_gg(X1, X2))
U48_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, lecH_out_gg(X1, X2)) → U49_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, qcG_in_ggggaa(X3, X2, X4, X5, X6, X8))
qcG_in_ggggaa(X1, X2, X3, [], .(X1, X3), X4) → U51_ggggaa(X1, X2, X3, X4, gtcI_in_gg(X1, X2))
gtcI_in_gg(s(X1), s(X2)) → U50_gg(X1, X2, gtcI_in_gg(X1, X2))
gtcI_in_gg(s(0), 0) → gtcI_out_gg(s(0), 0)
U50_gg(X1, X2, gtcI_out_gg(X1, X2)) → gtcI_out_gg(s(X1), s(X2))
U51_ggggaa(X1, X2, X3, X4, gtcI_out_gg(X1, X2)) → qcG_out_ggggaa(X1, X2, X3, [], .(X1, X3), X4)
qcG_in_ggggaa(X1, X2, X3, .(X4, X5), .(X1, X6), .(X7, X8)) → U52_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, gtcI_in_gg(X1, X2))
U52_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, gtcI_out_gg(X1, X2)) → U53_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, qcF_in_ggggaa(X1, X4, X3, X5, X6, X8))
U53_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, qcF_out_ggggaa(X1, X4, X3, X5, X6, X8)) → qcG_out_ggggaa(X1, X2, X3, .(X4, X5), .(X1, X6), .(X7, X8))
qcG_in_ggggaa(X1, X2, X3, .(X4, X5), .(X4, X6), .(X7, X8)) → U54_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, gtcI_in_gg(X1, X2))
U54_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, gtcI_out_gg(X1, X2)) → U55_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, qcG_in_ggggaa(X1, X4, X3, X5, X6, X8))
U55_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, qcG_out_ggggaa(X1, X4, X3, X5, X6, X8)) → qcG_out_ggggaa(X1, X2, X3, .(X4, X5), .(X4, X6), .(X7, X8))
U49_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, qcG_out_ggggaa(X3, X2, X4, X5, X6, X8)) → qcF_out_ggggaa(X1, X2, .(X3, X4), X5, .(X2, X6), .(X7, X8))
U47_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, qcF_out_ggggaa(X3, X2, X4, X5, X6, X8)) → qcF_out_ggggaa(X1, X2, .(X3, X4), X5, .(X3, X6), .(X7, X8))
U42_ggaaa(X1, X2, X3, X4, X5, X6, X7, qcF_out_ggggaa(X1, X3, X2, X4, X5, X7)) → mergecC_out_ggaaa(.(X1, X2), .(X3, X4), .(X1, X5), X6, X7)
mergecC_in_ggaaa(.(X1, X2), .(X3, X4), .(X3, X5), X6, X7) → U43_ggaaa(X1, X2, X3, X4, X5, X6, X7, qcG_in_ggggaa(X1, X3, X2, X4, X5, X7))
U43_ggaaa(X1, X2, X3, X4, X5, X6, X7, qcG_out_ggggaa(X1, X3, X2, X4, X5, X7)) → mergecC_out_ggaaa(.(X1, X2), .(X3, X4), .(X3, X5), X6, X7)
U41_gaa(X1, X2, X3, X4, X5, X6, mergecC_out_ggaaa(X9, X10, X4, X5, X6)) → mergesortcE_out_gaa(.(X1, .(X2, X3)), X4, .(X5, X6))
U35_gaa(X1, X2, X3, X4, X5, X6, X9, mergesortcE_out_gaa(X7, X10, X6)) → U36_gaa(X1, X2, X3, X4, X5, X6, mergecC_in_ggaaa(X9, X10, X4, X5, X6))
U36_gaa(X1, X2, X3, X4, X5, X6, mergecC_out_ggaaa(X9, X10, X4, X5, X6)) → mergesortcB_out_gaa(.(X1, .(X2, X3)), X4, .(X5, X6))

The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x1, x2)
splitcD_in_ggaaa(x1, x2, x3, x4, x5)  =  splitcD_in_ggaaa(x1, x2)
U37_ggaaa(x1, x2, x3, x4, x5, x6, x7)  =  U37_ggaaa(x1, x2, x7)
splitcA_in_gaaa(x1, x2, x3, x4)  =  splitcA_in_gaaa(x1)
[]  =  []
splitcA_out_gaaa(x1, x2, x3, x4)  =  splitcA_out_gaaa(x1, x2, x3)
U32_gaaa(x1, x2, x3, x4, x5, x6, x7)  =  U32_gaaa(x1, x2, x7)
splitcD_out_ggaaa(x1, x2, x3, x4, x5)  =  splitcD_out_ggaaa(x1, x2, x3, x4)
mergesortcB_in_gaa(x1, x2, x3)  =  mergesortcB_in_gaa(x1)
mergesortcB_out_gaa(x1, x2, x3)  =  mergesortcB_out_gaa(x1, x2)
U33_gaa(x1, x2, x3, x4, x5, x6, x7)  =  U33_gaa(x1, x2, x3, x7)
U34_gaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  U34_gaa(x1, x2, x3, x7, x8)
U35_gaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  U35_gaa(x1, x2, x3, x7, x8)
mergesortcE_in_gaa(x1, x2, x3)  =  mergesortcE_in_gaa(x1)
mergesortcE_out_gaa(x1, x2, x3)  =  mergesortcE_out_gaa(x1, x2)
U38_gaa(x1, x2, x3, x4, x5, x6, x7)  =  U38_gaa(x1, x2, x3, x7)
U39_gaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  U39_gaa(x1, x2, x3, x7, x8)
U40_gaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  U40_gaa(x1, x2, x3, x7, x8)
U41_gaa(x1, x2, x3, x4, x5, x6, x7)  =  U41_gaa(x1, x2, x3, x7)
mergecC_in_ggaaa(x1, x2, x3, x4, x5)  =  mergecC_in_ggaaa(x1, x2)
mergecC_out_ggaaa(x1, x2, x3, x4, x5)  =  mergecC_out_ggaaa(x1, x2, x3)
U42_ggaaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  U42_ggaaa(x1, x2, x3, x4, x8)
qcF_in_ggggaa(x1, x2, x3, x4, x5, x6)  =  qcF_in_ggggaa(x1, x2, x3, x4)
U45_ggggaa(x1, x2, x3, x4, x5)  =  U45_ggggaa(x1, x2, x3, x5)
lecH_in_gg(x1, x2)  =  lecH_in_gg(x1, x2)
s(x1)  =  s(x1)
U44_gg(x1, x2, x3)  =  U44_gg(x1, x2, x3)
0  =  0
lecH_out_gg(x1, x2)  =  lecH_out_gg(x1, x2)
qcF_out_ggggaa(x1, x2, x3, x4, x5, x6)  =  qcF_out_ggggaa(x1, x2, x3, x4, x5)
U46_ggggaa(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U46_ggggaa(x1, x2, x3, x4, x5, x9)
U47_ggggaa(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U47_ggggaa(x1, x2, x3, x4, x5, x9)
U48_ggggaa(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U48_ggggaa(x1, x2, x3, x4, x5, x9)
U49_ggggaa(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U49_ggggaa(x1, x2, x3, x4, x5, x9)
qcG_in_ggggaa(x1, x2, x3, x4, x5, x6)  =  qcG_in_ggggaa(x1, x2, x3, x4)
U51_ggggaa(x1, x2, x3, x4, x5)  =  U51_ggggaa(x1, x2, x3, x5)
gtcI_in_gg(x1, x2)  =  gtcI_in_gg(x1, x2)
U50_gg(x1, x2, x3)  =  U50_gg(x1, x2, x3)
gtcI_out_gg(x1, x2)  =  gtcI_out_gg(x1, x2)
qcG_out_ggggaa(x1, x2, x3, x4, x5, x6)  =  qcG_out_ggggaa(x1, x2, x3, x4, x5)
U52_ggggaa(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U52_ggggaa(x1, x2, x3, x4, x5, x9)
U53_ggggaa(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U53_ggggaa(x1, x2, x3, x4, x5, x9)
U54_ggggaa(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U54_ggggaa(x1, x2, x3, x4, x5, x9)
U55_ggggaa(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U55_ggggaa(x1, x2, x3, x4, x5, x9)
U43_ggaaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  U43_ggaaa(x1, x2, x3, x4, x8)
U36_gaa(x1, x2, x3, x4, x5, x6, x7)  =  U36_gaa(x1, x2, x3, x7)
GTI_IN_GG(x1, x2)  =  GTI_IN_GG(x1, x2)

We have to consider all (P,R,Pi)-chains

(8) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(9) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

GTI_IN_GG(s(X1), s(X2)) → GTI_IN_GG(X1, X2)

R is empty.
Pi is empty.
We have to consider all (P,R,Pi)-chains

(10) PiDPToQDPProof (EQUIVALENT transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(11) Obligation:

Q DP problem:
The TRS P consists of the following rules:

GTI_IN_GG(s(X1), s(X2)) → GTI_IN_GG(X1, X2)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(12) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

  • GTI_IN_GG(s(X1), s(X2)) → GTI_IN_GG(X1, X2)
    The graph contains the following edges 1 > 1, 2 > 2

(13) YES

(14) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

LEH_IN_GG(s(X1), s(X2)) → LEH_IN_GG(X1, X2)

The TRS R consists of the following rules:

splitcD_in_ggaaa(X1, X2, .(X1, X3), X4, .(X5, X6)) → U37_ggaaa(X1, X2, X3, X4, X5, X6, splitcA_in_gaaa(X2, X4, X3, X6))
splitcA_in_gaaa([], [], [], X1) → splitcA_out_gaaa([], [], [], X1)
splitcA_in_gaaa(.(X1, X2), .(X1, X3), X4, .(X5, X6)) → U32_gaaa(X1, X2, X3, X4, X5, X6, splitcA_in_gaaa(X2, X4, X3, X6))
U32_gaaa(X1, X2, X3, X4, X5, X6, splitcA_out_gaaa(X2, X4, X3, X6)) → splitcA_out_gaaa(.(X1, X2), .(X1, X3), X4, .(X5, X6))
U37_ggaaa(X1, X2, X3, X4, X5, X6, splitcA_out_gaaa(X2, X4, X3, X6)) → splitcD_out_ggaaa(X1, X2, .(X1, X3), X4, .(X5, X6))
mergesortcB_in_gaa([], [], X1) → mergesortcB_out_gaa([], [], X1)
mergesortcB_in_gaa(.(X1, []), .(X1, []), X2) → mergesortcB_out_gaa(.(X1, []), .(X1, []), X2)
mergesortcB_in_gaa(.(X1, .(X2, X3)), X4, .(X5, X6)) → U33_gaa(X1, X2, X3, X4, X5, X6, splitcD_in_ggaaa(X2, X3, X7, X8, X6))
U33_gaa(X1, X2, X3, X4, X5, X6, splitcD_out_ggaaa(X2, X3, X7, X8, X6)) → U34_gaa(X1, X2, X3, X4, X5, X6, X7, mergesortcB_in_gaa(.(X1, X8), X9, X6))
U34_gaa(X1, X2, X3, X4, X5, X6, X7, mergesortcB_out_gaa(.(X1, X8), X9, X6)) → U35_gaa(X1, X2, X3, X4, X5, X6, X9, mergesortcE_in_gaa(X7, X10, X6))
mergesortcE_in_gaa([], [], X1) → mergesortcE_out_gaa([], [], X1)
mergesortcE_in_gaa(.(X1, []), .(X1, []), X2) → mergesortcE_out_gaa(.(X1, []), .(X1, []), X2)
mergesortcE_in_gaa(.(X1, .(X2, X3)), X4, .(X5, X6)) → U38_gaa(X1, X2, X3, X4, X5, X6, splitcD_in_ggaaa(X1, .(X2, X3), X7, X8, .(X5, X6)))
U38_gaa(X1, X2, X3, X4, X5, X6, splitcD_out_ggaaa(X1, .(X2, X3), X7, X8, .(X5, X6))) → U39_gaa(X1, X2, X3, X4, X5, X6, X8, mergesortcE_in_gaa(X7, X9, X6))
U39_gaa(X1, X2, X3, X4, X5, X6, X8, mergesortcE_out_gaa(X7, X9, X6)) → U40_gaa(X1, X2, X3, X4, X5, X6, X9, mergesortcE_in_gaa(X8, X10, X6))
U40_gaa(X1, X2, X3, X4, X5, X6, X9, mergesortcE_out_gaa(X8, X10, X6)) → U41_gaa(X1, X2, X3, X4, X5, X6, mergecC_in_ggaaa(X9, X10, X4, X5, X6))
mergecC_in_ggaaa([], X1, X1, X2, X3) → mergecC_out_ggaaa([], X1, X1, X2, X3)
mergecC_in_ggaaa(X1, [], X1, X2, X3) → mergecC_out_ggaaa(X1, [], X1, X2, X3)
mergecC_in_ggaaa(.(X1, X2), .(X3, X4), .(X1, X5), X6, X7) → U42_ggaaa(X1, X2, X3, X4, X5, X6, X7, qcF_in_ggggaa(X1, X3, X2, X4, X5, X7))
qcF_in_ggggaa(X1, X2, [], X3, .(X2, X3), X4) → U45_ggggaa(X1, X2, X3, X4, lecH_in_gg(X1, X2))
lecH_in_gg(s(X1), s(X2)) → U44_gg(X1, X2, lecH_in_gg(X1, X2))
lecH_in_gg(0, s(0)) → lecH_out_gg(0, s(0))
lecH_in_gg(0, 0) → lecH_out_gg(0, 0)
U44_gg(X1, X2, lecH_out_gg(X1, X2)) → lecH_out_gg(s(X1), s(X2))
U45_ggggaa(X1, X2, X3, X4, lecH_out_gg(X1, X2)) → qcF_out_ggggaa(X1, X2, [], X3, .(X2, X3), X4)
qcF_in_ggggaa(X1, X2, .(X3, X4), X5, .(X3, X6), .(X7, X8)) → U46_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, lecH_in_gg(X1, X2))
U46_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, lecH_out_gg(X1, X2)) → U47_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, qcF_in_ggggaa(X3, X2, X4, X5, X6, X8))
qcF_in_ggggaa(X1, X2, .(X3, X4), X5, .(X2, X6), .(X7, X8)) → U48_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, lecH_in_gg(X1, X2))
U48_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, lecH_out_gg(X1, X2)) → U49_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, qcG_in_ggggaa(X3, X2, X4, X5, X6, X8))
qcG_in_ggggaa(X1, X2, X3, [], .(X1, X3), X4) → U51_ggggaa(X1, X2, X3, X4, gtcI_in_gg(X1, X2))
gtcI_in_gg(s(X1), s(X2)) → U50_gg(X1, X2, gtcI_in_gg(X1, X2))
gtcI_in_gg(s(0), 0) → gtcI_out_gg(s(0), 0)
U50_gg(X1, X2, gtcI_out_gg(X1, X2)) → gtcI_out_gg(s(X1), s(X2))
U51_ggggaa(X1, X2, X3, X4, gtcI_out_gg(X1, X2)) → qcG_out_ggggaa(X1, X2, X3, [], .(X1, X3), X4)
qcG_in_ggggaa(X1, X2, X3, .(X4, X5), .(X1, X6), .(X7, X8)) → U52_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, gtcI_in_gg(X1, X2))
U52_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, gtcI_out_gg(X1, X2)) → U53_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, qcF_in_ggggaa(X1, X4, X3, X5, X6, X8))
U53_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, qcF_out_ggggaa(X1, X4, X3, X5, X6, X8)) → qcG_out_ggggaa(X1, X2, X3, .(X4, X5), .(X1, X6), .(X7, X8))
qcG_in_ggggaa(X1, X2, X3, .(X4, X5), .(X4, X6), .(X7, X8)) → U54_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, gtcI_in_gg(X1, X2))
U54_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, gtcI_out_gg(X1, X2)) → U55_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, qcG_in_ggggaa(X1, X4, X3, X5, X6, X8))
U55_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, qcG_out_ggggaa(X1, X4, X3, X5, X6, X8)) → qcG_out_ggggaa(X1, X2, X3, .(X4, X5), .(X4, X6), .(X7, X8))
U49_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, qcG_out_ggggaa(X3, X2, X4, X5, X6, X8)) → qcF_out_ggggaa(X1, X2, .(X3, X4), X5, .(X2, X6), .(X7, X8))
U47_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, qcF_out_ggggaa(X3, X2, X4, X5, X6, X8)) → qcF_out_ggggaa(X1, X2, .(X3, X4), X5, .(X3, X6), .(X7, X8))
U42_ggaaa(X1, X2, X3, X4, X5, X6, X7, qcF_out_ggggaa(X1, X3, X2, X4, X5, X7)) → mergecC_out_ggaaa(.(X1, X2), .(X3, X4), .(X1, X5), X6, X7)
mergecC_in_ggaaa(.(X1, X2), .(X3, X4), .(X3, X5), X6, X7) → U43_ggaaa(X1, X2, X3, X4, X5, X6, X7, qcG_in_ggggaa(X1, X3, X2, X4, X5, X7))
U43_ggaaa(X1, X2, X3, X4, X5, X6, X7, qcG_out_ggggaa(X1, X3, X2, X4, X5, X7)) → mergecC_out_ggaaa(.(X1, X2), .(X3, X4), .(X3, X5), X6, X7)
U41_gaa(X1, X2, X3, X4, X5, X6, mergecC_out_ggaaa(X9, X10, X4, X5, X6)) → mergesortcE_out_gaa(.(X1, .(X2, X3)), X4, .(X5, X6))
U35_gaa(X1, X2, X3, X4, X5, X6, X9, mergesortcE_out_gaa(X7, X10, X6)) → U36_gaa(X1, X2, X3, X4, X5, X6, mergecC_in_ggaaa(X9, X10, X4, X5, X6))
U36_gaa(X1, X2, X3, X4, X5, X6, mergecC_out_ggaaa(X9, X10, X4, X5, X6)) → mergesortcB_out_gaa(.(X1, .(X2, X3)), X4, .(X5, X6))

The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x1, x2)
splitcD_in_ggaaa(x1, x2, x3, x4, x5)  =  splitcD_in_ggaaa(x1, x2)
U37_ggaaa(x1, x2, x3, x4, x5, x6, x7)  =  U37_ggaaa(x1, x2, x7)
splitcA_in_gaaa(x1, x2, x3, x4)  =  splitcA_in_gaaa(x1)
[]  =  []
splitcA_out_gaaa(x1, x2, x3, x4)  =  splitcA_out_gaaa(x1, x2, x3)
U32_gaaa(x1, x2, x3, x4, x5, x6, x7)  =  U32_gaaa(x1, x2, x7)
splitcD_out_ggaaa(x1, x2, x3, x4, x5)  =  splitcD_out_ggaaa(x1, x2, x3, x4)
mergesortcB_in_gaa(x1, x2, x3)  =  mergesortcB_in_gaa(x1)
mergesortcB_out_gaa(x1, x2, x3)  =  mergesortcB_out_gaa(x1, x2)
U33_gaa(x1, x2, x3, x4, x5, x6, x7)  =  U33_gaa(x1, x2, x3, x7)
U34_gaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  U34_gaa(x1, x2, x3, x7, x8)
U35_gaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  U35_gaa(x1, x2, x3, x7, x8)
mergesortcE_in_gaa(x1, x2, x3)  =  mergesortcE_in_gaa(x1)
mergesortcE_out_gaa(x1, x2, x3)  =  mergesortcE_out_gaa(x1, x2)
U38_gaa(x1, x2, x3, x4, x5, x6, x7)  =  U38_gaa(x1, x2, x3, x7)
U39_gaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  U39_gaa(x1, x2, x3, x7, x8)
U40_gaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  U40_gaa(x1, x2, x3, x7, x8)
U41_gaa(x1, x2, x3, x4, x5, x6, x7)  =  U41_gaa(x1, x2, x3, x7)
mergecC_in_ggaaa(x1, x2, x3, x4, x5)  =  mergecC_in_ggaaa(x1, x2)
mergecC_out_ggaaa(x1, x2, x3, x4, x5)  =  mergecC_out_ggaaa(x1, x2, x3)
U42_ggaaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  U42_ggaaa(x1, x2, x3, x4, x8)
qcF_in_ggggaa(x1, x2, x3, x4, x5, x6)  =  qcF_in_ggggaa(x1, x2, x3, x4)
U45_ggggaa(x1, x2, x3, x4, x5)  =  U45_ggggaa(x1, x2, x3, x5)
lecH_in_gg(x1, x2)  =  lecH_in_gg(x1, x2)
s(x1)  =  s(x1)
U44_gg(x1, x2, x3)  =  U44_gg(x1, x2, x3)
0  =  0
lecH_out_gg(x1, x2)  =  lecH_out_gg(x1, x2)
qcF_out_ggggaa(x1, x2, x3, x4, x5, x6)  =  qcF_out_ggggaa(x1, x2, x3, x4, x5)
U46_ggggaa(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U46_ggggaa(x1, x2, x3, x4, x5, x9)
U47_ggggaa(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U47_ggggaa(x1, x2, x3, x4, x5, x9)
U48_ggggaa(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U48_ggggaa(x1, x2, x3, x4, x5, x9)
U49_ggggaa(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U49_ggggaa(x1, x2, x3, x4, x5, x9)
qcG_in_ggggaa(x1, x2, x3, x4, x5, x6)  =  qcG_in_ggggaa(x1, x2, x3, x4)
U51_ggggaa(x1, x2, x3, x4, x5)  =  U51_ggggaa(x1, x2, x3, x5)
gtcI_in_gg(x1, x2)  =  gtcI_in_gg(x1, x2)
U50_gg(x1, x2, x3)  =  U50_gg(x1, x2, x3)
gtcI_out_gg(x1, x2)  =  gtcI_out_gg(x1, x2)
qcG_out_ggggaa(x1, x2, x3, x4, x5, x6)  =  qcG_out_ggggaa(x1, x2, x3, x4, x5)
U52_ggggaa(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U52_ggggaa(x1, x2, x3, x4, x5, x9)
U53_ggggaa(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U53_ggggaa(x1, x2, x3, x4, x5, x9)
U54_ggggaa(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U54_ggggaa(x1, x2, x3, x4, x5, x9)
U55_ggggaa(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U55_ggggaa(x1, x2, x3, x4, x5, x9)
U43_ggaaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  U43_ggaaa(x1, x2, x3, x4, x8)
U36_gaa(x1, x2, x3, x4, x5, x6, x7)  =  U36_gaa(x1, x2, x3, x7)
LEH_IN_GG(x1, x2)  =  LEH_IN_GG(x1, x2)

We have to consider all (P,R,Pi)-chains

(15) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(16) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

LEH_IN_GG(s(X1), s(X2)) → LEH_IN_GG(X1, X2)

R is empty.
Pi is empty.
We have to consider all (P,R,Pi)-chains

(17) PiDPToQDPProof (EQUIVALENT transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(18) Obligation:

Q DP problem:
The TRS P consists of the following rules:

LEH_IN_GG(s(X1), s(X2)) → LEH_IN_GG(X1, X2)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(19) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

  • LEH_IN_GG(s(X1), s(X2)) → LEH_IN_GG(X1, X2)
    The graph contains the following edges 1 > 1, 2 > 2

(20) YES

(21) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

PF_IN_GGGGAA(X1, X2, .(X3, X4), X5, .(X3, X6), .(X7, X8)) → U14_GGGGAA(X1, X2, X3, X4, X5, X6, X7, X8, lecH_in_gg(X1, X2))
U14_GGGGAA(X1, X2, X3, X4, X5, X6, X7, X8, lecH_out_gg(X1, X2)) → PF_IN_GGGGAA(X3, X2, X4, X5, X6, X8)
PF_IN_GGGGAA(X1, X2, .(X3, X4), X5, .(X2, X6), .(X7, X8)) → U16_GGGGAA(X1, X2, X3, X4, X5, X6, X7, X8, lecH_in_gg(X1, X2))
U16_GGGGAA(X1, X2, X3, X4, X5, X6, X7, X8, lecH_out_gg(X1, X2)) → PG_IN_GGGGAA(X3, X2, X4, X5, X6, X8)
PG_IN_GGGGAA(X1, X2, X3, .(X4, X5), .(X1, X6), .(X7, X8)) → U20_GGGGAA(X1, X2, X3, X4, X5, X6, X7, X8, gtcI_in_gg(X1, X2))
U20_GGGGAA(X1, X2, X3, X4, X5, X6, X7, X8, gtcI_out_gg(X1, X2)) → PF_IN_GGGGAA(X1, X4, X3, X5, X6, X8)
PG_IN_GGGGAA(X1, X2, X3, .(X4, X5), .(X4, X6), .(X7, X8)) → U22_GGGGAA(X1, X2, X3, X4, X5, X6, X7, X8, gtcI_in_gg(X1, X2))
U22_GGGGAA(X1, X2, X3, X4, X5, X6, X7, X8, gtcI_out_gg(X1, X2)) → PG_IN_GGGGAA(X1, X4, X3, X5, X6, X8)

The TRS R consists of the following rules:

splitcD_in_ggaaa(X1, X2, .(X1, X3), X4, .(X5, X6)) → U37_ggaaa(X1, X2, X3, X4, X5, X6, splitcA_in_gaaa(X2, X4, X3, X6))
splitcA_in_gaaa([], [], [], X1) → splitcA_out_gaaa([], [], [], X1)
splitcA_in_gaaa(.(X1, X2), .(X1, X3), X4, .(X5, X6)) → U32_gaaa(X1, X2, X3, X4, X5, X6, splitcA_in_gaaa(X2, X4, X3, X6))
U32_gaaa(X1, X2, X3, X4, X5, X6, splitcA_out_gaaa(X2, X4, X3, X6)) → splitcA_out_gaaa(.(X1, X2), .(X1, X3), X4, .(X5, X6))
U37_ggaaa(X1, X2, X3, X4, X5, X6, splitcA_out_gaaa(X2, X4, X3, X6)) → splitcD_out_ggaaa(X1, X2, .(X1, X3), X4, .(X5, X6))
mergesortcB_in_gaa([], [], X1) → mergesortcB_out_gaa([], [], X1)
mergesortcB_in_gaa(.(X1, []), .(X1, []), X2) → mergesortcB_out_gaa(.(X1, []), .(X1, []), X2)
mergesortcB_in_gaa(.(X1, .(X2, X3)), X4, .(X5, X6)) → U33_gaa(X1, X2, X3, X4, X5, X6, splitcD_in_ggaaa(X2, X3, X7, X8, X6))
U33_gaa(X1, X2, X3, X4, X5, X6, splitcD_out_ggaaa(X2, X3, X7, X8, X6)) → U34_gaa(X1, X2, X3, X4, X5, X6, X7, mergesortcB_in_gaa(.(X1, X8), X9, X6))
U34_gaa(X1, X2, X3, X4, X5, X6, X7, mergesortcB_out_gaa(.(X1, X8), X9, X6)) → U35_gaa(X1, X2, X3, X4, X5, X6, X9, mergesortcE_in_gaa(X7, X10, X6))
mergesortcE_in_gaa([], [], X1) → mergesortcE_out_gaa([], [], X1)
mergesortcE_in_gaa(.(X1, []), .(X1, []), X2) → mergesortcE_out_gaa(.(X1, []), .(X1, []), X2)
mergesortcE_in_gaa(.(X1, .(X2, X3)), X4, .(X5, X6)) → U38_gaa(X1, X2, X3, X4, X5, X6, splitcD_in_ggaaa(X1, .(X2, X3), X7, X8, .(X5, X6)))
U38_gaa(X1, X2, X3, X4, X5, X6, splitcD_out_ggaaa(X1, .(X2, X3), X7, X8, .(X5, X6))) → U39_gaa(X1, X2, X3, X4, X5, X6, X8, mergesortcE_in_gaa(X7, X9, X6))
U39_gaa(X1, X2, X3, X4, X5, X6, X8, mergesortcE_out_gaa(X7, X9, X6)) → U40_gaa(X1, X2, X3, X4, X5, X6, X9, mergesortcE_in_gaa(X8, X10, X6))
U40_gaa(X1, X2, X3, X4, X5, X6, X9, mergesortcE_out_gaa(X8, X10, X6)) → U41_gaa(X1, X2, X3, X4, X5, X6, mergecC_in_ggaaa(X9, X10, X4, X5, X6))
mergecC_in_ggaaa([], X1, X1, X2, X3) → mergecC_out_ggaaa([], X1, X1, X2, X3)
mergecC_in_ggaaa(X1, [], X1, X2, X3) → mergecC_out_ggaaa(X1, [], X1, X2, X3)
mergecC_in_ggaaa(.(X1, X2), .(X3, X4), .(X1, X5), X6, X7) → U42_ggaaa(X1, X2, X3, X4, X5, X6, X7, qcF_in_ggggaa(X1, X3, X2, X4, X5, X7))
qcF_in_ggggaa(X1, X2, [], X3, .(X2, X3), X4) → U45_ggggaa(X1, X2, X3, X4, lecH_in_gg(X1, X2))
lecH_in_gg(s(X1), s(X2)) → U44_gg(X1, X2, lecH_in_gg(X1, X2))
lecH_in_gg(0, s(0)) → lecH_out_gg(0, s(0))
lecH_in_gg(0, 0) → lecH_out_gg(0, 0)
U44_gg(X1, X2, lecH_out_gg(X1, X2)) → lecH_out_gg(s(X1), s(X2))
U45_ggggaa(X1, X2, X3, X4, lecH_out_gg(X1, X2)) → qcF_out_ggggaa(X1, X2, [], X3, .(X2, X3), X4)
qcF_in_ggggaa(X1, X2, .(X3, X4), X5, .(X3, X6), .(X7, X8)) → U46_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, lecH_in_gg(X1, X2))
U46_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, lecH_out_gg(X1, X2)) → U47_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, qcF_in_ggggaa(X3, X2, X4, X5, X6, X8))
qcF_in_ggggaa(X1, X2, .(X3, X4), X5, .(X2, X6), .(X7, X8)) → U48_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, lecH_in_gg(X1, X2))
U48_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, lecH_out_gg(X1, X2)) → U49_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, qcG_in_ggggaa(X3, X2, X4, X5, X6, X8))
qcG_in_ggggaa(X1, X2, X3, [], .(X1, X3), X4) → U51_ggggaa(X1, X2, X3, X4, gtcI_in_gg(X1, X2))
gtcI_in_gg(s(X1), s(X2)) → U50_gg(X1, X2, gtcI_in_gg(X1, X2))
gtcI_in_gg(s(0), 0) → gtcI_out_gg(s(0), 0)
U50_gg(X1, X2, gtcI_out_gg(X1, X2)) → gtcI_out_gg(s(X1), s(X2))
U51_ggggaa(X1, X2, X3, X4, gtcI_out_gg(X1, X2)) → qcG_out_ggggaa(X1, X2, X3, [], .(X1, X3), X4)
qcG_in_ggggaa(X1, X2, X3, .(X4, X5), .(X1, X6), .(X7, X8)) → U52_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, gtcI_in_gg(X1, X2))
U52_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, gtcI_out_gg(X1, X2)) → U53_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, qcF_in_ggggaa(X1, X4, X3, X5, X6, X8))
U53_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, qcF_out_ggggaa(X1, X4, X3, X5, X6, X8)) → qcG_out_ggggaa(X1, X2, X3, .(X4, X5), .(X1, X6), .(X7, X8))
qcG_in_ggggaa(X1, X2, X3, .(X4, X5), .(X4, X6), .(X7, X8)) → U54_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, gtcI_in_gg(X1, X2))
U54_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, gtcI_out_gg(X1, X2)) → U55_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, qcG_in_ggggaa(X1, X4, X3, X5, X6, X8))
U55_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, qcG_out_ggggaa(X1, X4, X3, X5, X6, X8)) → qcG_out_ggggaa(X1, X2, X3, .(X4, X5), .(X4, X6), .(X7, X8))
U49_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, qcG_out_ggggaa(X3, X2, X4, X5, X6, X8)) → qcF_out_ggggaa(X1, X2, .(X3, X4), X5, .(X2, X6), .(X7, X8))
U47_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, qcF_out_ggggaa(X3, X2, X4, X5, X6, X8)) → qcF_out_ggggaa(X1, X2, .(X3, X4), X5, .(X3, X6), .(X7, X8))
U42_ggaaa(X1, X2, X3, X4, X5, X6, X7, qcF_out_ggggaa(X1, X3, X2, X4, X5, X7)) → mergecC_out_ggaaa(.(X1, X2), .(X3, X4), .(X1, X5), X6, X7)
mergecC_in_ggaaa(.(X1, X2), .(X3, X4), .(X3, X5), X6, X7) → U43_ggaaa(X1, X2, X3, X4, X5, X6, X7, qcG_in_ggggaa(X1, X3, X2, X4, X5, X7))
U43_ggaaa(X1, X2, X3, X4, X5, X6, X7, qcG_out_ggggaa(X1, X3, X2, X4, X5, X7)) → mergecC_out_ggaaa(.(X1, X2), .(X3, X4), .(X3, X5), X6, X7)
U41_gaa(X1, X2, X3, X4, X5, X6, mergecC_out_ggaaa(X9, X10, X4, X5, X6)) → mergesortcE_out_gaa(.(X1, .(X2, X3)), X4, .(X5, X6))
U35_gaa(X1, X2, X3, X4, X5, X6, X9, mergesortcE_out_gaa(X7, X10, X6)) → U36_gaa(X1, X2, X3, X4, X5, X6, mergecC_in_ggaaa(X9, X10, X4, X5, X6))
U36_gaa(X1, X2, X3, X4, X5, X6, mergecC_out_ggaaa(X9, X10, X4, X5, X6)) → mergesortcB_out_gaa(.(X1, .(X2, X3)), X4, .(X5, X6))

The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x1, x2)
splitcD_in_ggaaa(x1, x2, x3, x4, x5)  =  splitcD_in_ggaaa(x1, x2)
U37_ggaaa(x1, x2, x3, x4, x5, x6, x7)  =  U37_ggaaa(x1, x2, x7)
splitcA_in_gaaa(x1, x2, x3, x4)  =  splitcA_in_gaaa(x1)
[]  =  []
splitcA_out_gaaa(x1, x2, x3, x4)  =  splitcA_out_gaaa(x1, x2, x3)
U32_gaaa(x1, x2, x3, x4, x5, x6, x7)  =  U32_gaaa(x1, x2, x7)
splitcD_out_ggaaa(x1, x2, x3, x4, x5)  =  splitcD_out_ggaaa(x1, x2, x3, x4)
mergesortcB_in_gaa(x1, x2, x3)  =  mergesortcB_in_gaa(x1)
mergesortcB_out_gaa(x1, x2, x3)  =  mergesortcB_out_gaa(x1, x2)
U33_gaa(x1, x2, x3, x4, x5, x6, x7)  =  U33_gaa(x1, x2, x3, x7)
U34_gaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  U34_gaa(x1, x2, x3, x7, x8)
U35_gaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  U35_gaa(x1, x2, x3, x7, x8)
mergesortcE_in_gaa(x1, x2, x3)  =  mergesortcE_in_gaa(x1)
mergesortcE_out_gaa(x1, x2, x3)  =  mergesortcE_out_gaa(x1, x2)
U38_gaa(x1, x2, x3, x4, x5, x6, x7)  =  U38_gaa(x1, x2, x3, x7)
U39_gaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  U39_gaa(x1, x2, x3, x7, x8)
U40_gaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  U40_gaa(x1, x2, x3, x7, x8)
U41_gaa(x1, x2, x3, x4, x5, x6, x7)  =  U41_gaa(x1, x2, x3, x7)
mergecC_in_ggaaa(x1, x2, x3, x4, x5)  =  mergecC_in_ggaaa(x1, x2)
mergecC_out_ggaaa(x1, x2, x3, x4, x5)  =  mergecC_out_ggaaa(x1, x2, x3)
U42_ggaaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  U42_ggaaa(x1, x2, x3, x4, x8)
qcF_in_ggggaa(x1, x2, x3, x4, x5, x6)  =  qcF_in_ggggaa(x1, x2, x3, x4)
U45_ggggaa(x1, x2, x3, x4, x5)  =  U45_ggggaa(x1, x2, x3, x5)
lecH_in_gg(x1, x2)  =  lecH_in_gg(x1, x2)
s(x1)  =  s(x1)
U44_gg(x1, x2, x3)  =  U44_gg(x1, x2, x3)
0  =  0
lecH_out_gg(x1, x2)  =  lecH_out_gg(x1, x2)
qcF_out_ggggaa(x1, x2, x3, x4, x5, x6)  =  qcF_out_ggggaa(x1, x2, x3, x4, x5)
U46_ggggaa(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U46_ggggaa(x1, x2, x3, x4, x5, x9)
U47_ggggaa(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U47_ggggaa(x1, x2, x3, x4, x5, x9)
U48_ggggaa(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U48_ggggaa(x1, x2, x3, x4, x5, x9)
U49_ggggaa(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U49_ggggaa(x1, x2, x3, x4, x5, x9)
qcG_in_ggggaa(x1, x2, x3, x4, x5, x6)  =  qcG_in_ggggaa(x1, x2, x3, x4)
U51_ggggaa(x1, x2, x3, x4, x5)  =  U51_ggggaa(x1, x2, x3, x5)
gtcI_in_gg(x1, x2)  =  gtcI_in_gg(x1, x2)
U50_gg(x1, x2, x3)  =  U50_gg(x1, x2, x3)
gtcI_out_gg(x1, x2)  =  gtcI_out_gg(x1, x2)
qcG_out_ggggaa(x1, x2, x3, x4, x5, x6)  =  qcG_out_ggggaa(x1, x2, x3, x4, x5)
U52_ggggaa(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U52_ggggaa(x1, x2, x3, x4, x5, x9)
U53_ggggaa(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U53_ggggaa(x1, x2, x3, x4, x5, x9)
U54_ggggaa(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U54_ggggaa(x1, x2, x3, x4, x5, x9)
U55_ggggaa(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U55_ggggaa(x1, x2, x3, x4, x5, x9)
U43_ggaaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  U43_ggaaa(x1, x2, x3, x4, x8)
U36_gaa(x1, x2, x3, x4, x5, x6, x7)  =  U36_gaa(x1, x2, x3, x7)
PF_IN_GGGGAA(x1, x2, x3, x4, x5, x6)  =  PF_IN_GGGGAA(x1, x2, x3, x4)
U14_GGGGAA(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U14_GGGGAA(x1, x2, x3, x4, x5, x9)
U16_GGGGAA(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U16_GGGGAA(x1, x2, x3, x4, x5, x9)
PG_IN_GGGGAA(x1, x2, x3, x4, x5, x6)  =  PG_IN_GGGGAA(x1, x2, x3, x4)
U20_GGGGAA(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U20_GGGGAA(x1, x2, x3, x4, x5, x9)
U22_GGGGAA(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U22_GGGGAA(x1, x2, x3, x4, x5, x9)

We have to consider all (P,R,Pi)-chains

(22) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(23) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

PF_IN_GGGGAA(X1, X2, .(X3, X4), X5, .(X3, X6), .(X7, X8)) → U14_GGGGAA(X1, X2, X3, X4, X5, X6, X7, X8, lecH_in_gg(X1, X2))
U14_GGGGAA(X1, X2, X3, X4, X5, X6, X7, X8, lecH_out_gg(X1, X2)) → PF_IN_GGGGAA(X3, X2, X4, X5, X6, X8)
PF_IN_GGGGAA(X1, X2, .(X3, X4), X5, .(X2, X6), .(X7, X8)) → U16_GGGGAA(X1, X2, X3, X4, X5, X6, X7, X8, lecH_in_gg(X1, X2))
U16_GGGGAA(X1, X2, X3, X4, X5, X6, X7, X8, lecH_out_gg(X1, X2)) → PG_IN_GGGGAA(X3, X2, X4, X5, X6, X8)
PG_IN_GGGGAA(X1, X2, X3, .(X4, X5), .(X1, X6), .(X7, X8)) → U20_GGGGAA(X1, X2, X3, X4, X5, X6, X7, X8, gtcI_in_gg(X1, X2))
U20_GGGGAA(X1, X2, X3, X4, X5, X6, X7, X8, gtcI_out_gg(X1, X2)) → PF_IN_GGGGAA(X1, X4, X3, X5, X6, X8)
PG_IN_GGGGAA(X1, X2, X3, .(X4, X5), .(X4, X6), .(X7, X8)) → U22_GGGGAA(X1, X2, X3, X4, X5, X6, X7, X8, gtcI_in_gg(X1, X2))
U22_GGGGAA(X1, X2, X3, X4, X5, X6, X7, X8, gtcI_out_gg(X1, X2)) → PG_IN_GGGGAA(X1, X4, X3, X5, X6, X8)

The TRS R consists of the following rules:

lecH_in_gg(s(X1), s(X2)) → U44_gg(X1, X2, lecH_in_gg(X1, X2))
lecH_in_gg(0, s(0)) → lecH_out_gg(0, s(0))
lecH_in_gg(0, 0) → lecH_out_gg(0, 0)
gtcI_in_gg(s(X1), s(X2)) → U50_gg(X1, X2, gtcI_in_gg(X1, X2))
gtcI_in_gg(s(0), 0) → gtcI_out_gg(s(0), 0)
U44_gg(X1, X2, lecH_out_gg(X1, X2)) → lecH_out_gg(s(X1), s(X2))
U50_gg(X1, X2, gtcI_out_gg(X1, X2)) → gtcI_out_gg(s(X1), s(X2))

The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x1, x2)
lecH_in_gg(x1, x2)  =  lecH_in_gg(x1, x2)
s(x1)  =  s(x1)
U44_gg(x1, x2, x3)  =  U44_gg(x1, x2, x3)
0  =  0
lecH_out_gg(x1, x2)  =  lecH_out_gg(x1, x2)
gtcI_in_gg(x1, x2)  =  gtcI_in_gg(x1, x2)
U50_gg(x1, x2, x3)  =  U50_gg(x1, x2, x3)
gtcI_out_gg(x1, x2)  =  gtcI_out_gg(x1, x2)
PF_IN_GGGGAA(x1, x2, x3, x4, x5, x6)  =  PF_IN_GGGGAA(x1, x2, x3, x4)
U14_GGGGAA(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U14_GGGGAA(x1, x2, x3, x4, x5, x9)
U16_GGGGAA(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U16_GGGGAA(x1, x2, x3, x4, x5, x9)
PG_IN_GGGGAA(x1, x2, x3, x4, x5, x6)  =  PG_IN_GGGGAA(x1, x2, x3, x4)
U20_GGGGAA(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U20_GGGGAA(x1, x2, x3, x4, x5, x9)
U22_GGGGAA(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U22_GGGGAA(x1, x2, x3, x4, x5, x9)

We have to consider all (P,R,Pi)-chains

(24) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(25) Obligation:

Q DP problem:
The TRS P consists of the following rules:

PF_IN_GGGGAA(X1, X2, .(X3, X4), X5) → U14_GGGGAA(X1, X2, X3, X4, X5, lecH_in_gg(X1, X2))
U14_GGGGAA(X1, X2, X3, X4, X5, lecH_out_gg(X1, X2)) → PF_IN_GGGGAA(X3, X2, X4, X5)
PF_IN_GGGGAA(X1, X2, .(X3, X4), X5) → U16_GGGGAA(X1, X2, X3, X4, X5, lecH_in_gg(X1, X2))
U16_GGGGAA(X1, X2, X3, X4, X5, lecH_out_gg(X1, X2)) → PG_IN_GGGGAA(X3, X2, X4, X5)
PG_IN_GGGGAA(X1, X2, X3, .(X4, X5)) → U20_GGGGAA(X1, X2, X3, X4, X5, gtcI_in_gg(X1, X2))
U20_GGGGAA(X1, X2, X3, X4, X5, gtcI_out_gg(X1, X2)) → PF_IN_GGGGAA(X1, X4, X3, X5)
PG_IN_GGGGAA(X1, X2, X3, .(X4, X5)) → U22_GGGGAA(X1, X2, X3, X4, X5, gtcI_in_gg(X1, X2))
U22_GGGGAA(X1, X2, X3, X4, X5, gtcI_out_gg(X1, X2)) → PG_IN_GGGGAA(X1, X4, X3, X5)

The TRS R consists of the following rules:

lecH_in_gg(s(X1), s(X2)) → U44_gg(X1, X2, lecH_in_gg(X1, X2))
lecH_in_gg(0, s(0)) → lecH_out_gg(0, s(0))
lecH_in_gg(0, 0) → lecH_out_gg(0, 0)
gtcI_in_gg(s(X1), s(X2)) → U50_gg(X1, X2, gtcI_in_gg(X1, X2))
gtcI_in_gg(s(0), 0) → gtcI_out_gg(s(0), 0)
U44_gg(X1, X2, lecH_out_gg(X1, X2)) → lecH_out_gg(s(X1), s(X2))
U50_gg(X1, X2, gtcI_out_gg(X1, X2)) → gtcI_out_gg(s(X1), s(X2))

The set Q consists of the following terms:

lecH_in_gg(x0, x1)
gtcI_in_gg(x0, x1)
U44_gg(x0, x1, x2)
U50_gg(x0, x1, x2)

We have to consider all (P,Q,R)-chains.

(26) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

  • U14_GGGGAA(X1, X2, X3, X4, X5, lecH_out_gg(X1, X2)) → PF_IN_GGGGAA(X3, X2, X4, X5)
    The graph contains the following edges 3 >= 1, 2 >= 2, 6 > 2, 4 >= 3, 5 >= 4

  • U20_GGGGAA(X1, X2, X3, X4, X5, gtcI_out_gg(X1, X2)) → PF_IN_GGGGAA(X1, X4, X3, X5)
    The graph contains the following edges 1 >= 1, 6 > 1, 4 >= 2, 3 >= 3, 5 >= 4

  • PF_IN_GGGGAA(X1, X2, .(X3, X4), X5) → U14_GGGGAA(X1, X2, X3, X4, X5, lecH_in_gg(X1, X2))
    The graph contains the following edges 1 >= 1, 2 >= 2, 3 > 3, 3 > 4, 4 >= 5

  • PF_IN_GGGGAA(X1, X2, .(X3, X4), X5) → U16_GGGGAA(X1, X2, X3, X4, X5, lecH_in_gg(X1, X2))
    The graph contains the following edges 1 >= 1, 2 >= 2, 3 > 3, 3 > 4, 4 >= 5

  • U16_GGGGAA(X1, X2, X3, X4, X5, lecH_out_gg(X1, X2)) → PG_IN_GGGGAA(X3, X2, X4, X5)
    The graph contains the following edges 3 >= 1, 2 >= 2, 6 > 2, 4 >= 3, 5 >= 4

  • U22_GGGGAA(X1, X2, X3, X4, X5, gtcI_out_gg(X1, X2)) → PG_IN_GGGGAA(X1, X4, X3, X5)
    The graph contains the following edges 1 >= 1, 6 > 1, 4 >= 2, 3 >= 3, 5 >= 4

  • PG_IN_GGGGAA(X1, X2, X3, .(X4, X5)) → U20_GGGGAA(X1, X2, X3, X4, X5, gtcI_in_gg(X1, X2))
    The graph contains the following edges 1 >= 1, 2 >= 2, 3 >= 3, 4 > 4, 4 > 5

  • PG_IN_GGGGAA(X1, X2, X3, .(X4, X5)) → U22_GGGGAA(X1, X2, X3, X4, X5, gtcI_in_gg(X1, X2))
    The graph contains the following edges 1 >= 1, 2 >= 2, 3 >= 3, 4 > 4, 4 > 5

(27) YES

(28) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

SPLITA_IN_GAAA(.(X1, X2), .(X1, X3), X4, .(X5, X6)) → SPLITA_IN_GAAA(X2, X4, X3, X6)

The TRS R consists of the following rules:

splitcD_in_ggaaa(X1, X2, .(X1, X3), X4, .(X5, X6)) → U37_ggaaa(X1, X2, X3, X4, X5, X6, splitcA_in_gaaa(X2, X4, X3, X6))
splitcA_in_gaaa([], [], [], X1) → splitcA_out_gaaa([], [], [], X1)
splitcA_in_gaaa(.(X1, X2), .(X1, X3), X4, .(X5, X6)) → U32_gaaa(X1, X2, X3, X4, X5, X6, splitcA_in_gaaa(X2, X4, X3, X6))
U32_gaaa(X1, X2, X3, X4, X5, X6, splitcA_out_gaaa(X2, X4, X3, X6)) → splitcA_out_gaaa(.(X1, X2), .(X1, X3), X4, .(X5, X6))
U37_ggaaa(X1, X2, X3, X4, X5, X6, splitcA_out_gaaa(X2, X4, X3, X6)) → splitcD_out_ggaaa(X1, X2, .(X1, X3), X4, .(X5, X6))
mergesortcB_in_gaa([], [], X1) → mergesortcB_out_gaa([], [], X1)
mergesortcB_in_gaa(.(X1, []), .(X1, []), X2) → mergesortcB_out_gaa(.(X1, []), .(X1, []), X2)
mergesortcB_in_gaa(.(X1, .(X2, X3)), X4, .(X5, X6)) → U33_gaa(X1, X2, X3, X4, X5, X6, splitcD_in_ggaaa(X2, X3, X7, X8, X6))
U33_gaa(X1, X2, X3, X4, X5, X6, splitcD_out_ggaaa(X2, X3, X7, X8, X6)) → U34_gaa(X1, X2, X3, X4, X5, X6, X7, mergesortcB_in_gaa(.(X1, X8), X9, X6))
U34_gaa(X1, X2, X3, X4, X5, X6, X7, mergesortcB_out_gaa(.(X1, X8), X9, X6)) → U35_gaa(X1, X2, X3, X4, X5, X6, X9, mergesortcE_in_gaa(X7, X10, X6))
mergesortcE_in_gaa([], [], X1) → mergesortcE_out_gaa([], [], X1)
mergesortcE_in_gaa(.(X1, []), .(X1, []), X2) → mergesortcE_out_gaa(.(X1, []), .(X1, []), X2)
mergesortcE_in_gaa(.(X1, .(X2, X3)), X4, .(X5, X6)) → U38_gaa(X1, X2, X3, X4, X5, X6, splitcD_in_ggaaa(X1, .(X2, X3), X7, X8, .(X5, X6)))
U38_gaa(X1, X2, X3, X4, X5, X6, splitcD_out_ggaaa(X1, .(X2, X3), X7, X8, .(X5, X6))) → U39_gaa(X1, X2, X3, X4, X5, X6, X8, mergesortcE_in_gaa(X7, X9, X6))
U39_gaa(X1, X2, X3, X4, X5, X6, X8, mergesortcE_out_gaa(X7, X9, X6)) → U40_gaa(X1, X2, X3, X4, X5, X6, X9, mergesortcE_in_gaa(X8, X10, X6))
U40_gaa(X1, X2, X3, X4, X5, X6, X9, mergesortcE_out_gaa(X8, X10, X6)) → U41_gaa(X1, X2, X3, X4, X5, X6, mergecC_in_ggaaa(X9, X10, X4, X5, X6))
mergecC_in_ggaaa([], X1, X1, X2, X3) → mergecC_out_ggaaa([], X1, X1, X2, X3)
mergecC_in_ggaaa(X1, [], X1, X2, X3) → mergecC_out_ggaaa(X1, [], X1, X2, X3)
mergecC_in_ggaaa(.(X1, X2), .(X3, X4), .(X1, X5), X6, X7) → U42_ggaaa(X1, X2, X3, X4, X5, X6, X7, qcF_in_ggggaa(X1, X3, X2, X4, X5, X7))
qcF_in_ggggaa(X1, X2, [], X3, .(X2, X3), X4) → U45_ggggaa(X1, X2, X3, X4, lecH_in_gg(X1, X2))
lecH_in_gg(s(X1), s(X2)) → U44_gg(X1, X2, lecH_in_gg(X1, X2))
lecH_in_gg(0, s(0)) → lecH_out_gg(0, s(0))
lecH_in_gg(0, 0) → lecH_out_gg(0, 0)
U44_gg(X1, X2, lecH_out_gg(X1, X2)) → lecH_out_gg(s(X1), s(X2))
U45_ggggaa(X1, X2, X3, X4, lecH_out_gg(X1, X2)) → qcF_out_ggggaa(X1, X2, [], X3, .(X2, X3), X4)
qcF_in_ggggaa(X1, X2, .(X3, X4), X5, .(X3, X6), .(X7, X8)) → U46_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, lecH_in_gg(X1, X2))
U46_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, lecH_out_gg(X1, X2)) → U47_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, qcF_in_ggggaa(X3, X2, X4, X5, X6, X8))
qcF_in_ggggaa(X1, X2, .(X3, X4), X5, .(X2, X6), .(X7, X8)) → U48_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, lecH_in_gg(X1, X2))
U48_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, lecH_out_gg(X1, X2)) → U49_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, qcG_in_ggggaa(X3, X2, X4, X5, X6, X8))
qcG_in_ggggaa(X1, X2, X3, [], .(X1, X3), X4) → U51_ggggaa(X1, X2, X3, X4, gtcI_in_gg(X1, X2))
gtcI_in_gg(s(X1), s(X2)) → U50_gg(X1, X2, gtcI_in_gg(X1, X2))
gtcI_in_gg(s(0), 0) → gtcI_out_gg(s(0), 0)
U50_gg(X1, X2, gtcI_out_gg(X1, X2)) → gtcI_out_gg(s(X1), s(X2))
U51_ggggaa(X1, X2, X3, X4, gtcI_out_gg(X1, X2)) → qcG_out_ggggaa(X1, X2, X3, [], .(X1, X3), X4)
qcG_in_ggggaa(X1, X2, X3, .(X4, X5), .(X1, X6), .(X7, X8)) → U52_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, gtcI_in_gg(X1, X2))
U52_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, gtcI_out_gg(X1, X2)) → U53_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, qcF_in_ggggaa(X1, X4, X3, X5, X6, X8))
U53_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, qcF_out_ggggaa(X1, X4, X3, X5, X6, X8)) → qcG_out_ggggaa(X1, X2, X3, .(X4, X5), .(X1, X6), .(X7, X8))
qcG_in_ggggaa(X1, X2, X3, .(X4, X5), .(X4, X6), .(X7, X8)) → U54_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, gtcI_in_gg(X1, X2))
U54_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, gtcI_out_gg(X1, X2)) → U55_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, qcG_in_ggggaa(X1, X4, X3, X5, X6, X8))
U55_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, qcG_out_ggggaa(X1, X4, X3, X5, X6, X8)) → qcG_out_ggggaa(X1, X2, X3, .(X4, X5), .(X4, X6), .(X7, X8))
U49_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, qcG_out_ggggaa(X3, X2, X4, X5, X6, X8)) → qcF_out_ggggaa(X1, X2, .(X3, X4), X5, .(X2, X6), .(X7, X8))
U47_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, qcF_out_ggggaa(X3, X2, X4, X5, X6, X8)) → qcF_out_ggggaa(X1, X2, .(X3, X4), X5, .(X3, X6), .(X7, X8))
U42_ggaaa(X1, X2, X3, X4, X5, X6, X7, qcF_out_ggggaa(X1, X3, X2, X4, X5, X7)) → mergecC_out_ggaaa(.(X1, X2), .(X3, X4), .(X1, X5), X6, X7)
mergecC_in_ggaaa(.(X1, X2), .(X3, X4), .(X3, X5), X6, X7) → U43_ggaaa(X1, X2, X3, X4, X5, X6, X7, qcG_in_ggggaa(X1, X3, X2, X4, X5, X7))
U43_ggaaa(X1, X2, X3, X4, X5, X6, X7, qcG_out_ggggaa(X1, X3, X2, X4, X5, X7)) → mergecC_out_ggaaa(.(X1, X2), .(X3, X4), .(X3, X5), X6, X7)
U41_gaa(X1, X2, X3, X4, X5, X6, mergecC_out_ggaaa(X9, X10, X4, X5, X6)) → mergesortcE_out_gaa(.(X1, .(X2, X3)), X4, .(X5, X6))
U35_gaa(X1, X2, X3, X4, X5, X6, X9, mergesortcE_out_gaa(X7, X10, X6)) → U36_gaa(X1, X2, X3, X4, X5, X6, mergecC_in_ggaaa(X9, X10, X4, X5, X6))
U36_gaa(X1, X2, X3, X4, X5, X6, mergecC_out_ggaaa(X9, X10, X4, X5, X6)) → mergesortcB_out_gaa(.(X1, .(X2, X3)), X4, .(X5, X6))

The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x1, x2)
splitcD_in_ggaaa(x1, x2, x3, x4, x5)  =  splitcD_in_ggaaa(x1, x2)
U37_ggaaa(x1, x2, x3, x4, x5, x6, x7)  =  U37_ggaaa(x1, x2, x7)
splitcA_in_gaaa(x1, x2, x3, x4)  =  splitcA_in_gaaa(x1)
[]  =  []
splitcA_out_gaaa(x1, x2, x3, x4)  =  splitcA_out_gaaa(x1, x2, x3)
U32_gaaa(x1, x2, x3, x4, x5, x6, x7)  =  U32_gaaa(x1, x2, x7)
splitcD_out_ggaaa(x1, x2, x3, x4, x5)  =  splitcD_out_ggaaa(x1, x2, x3, x4)
mergesortcB_in_gaa(x1, x2, x3)  =  mergesortcB_in_gaa(x1)
mergesortcB_out_gaa(x1, x2, x3)  =  mergesortcB_out_gaa(x1, x2)
U33_gaa(x1, x2, x3, x4, x5, x6, x7)  =  U33_gaa(x1, x2, x3, x7)
U34_gaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  U34_gaa(x1, x2, x3, x7, x8)
U35_gaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  U35_gaa(x1, x2, x3, x7, x8)
mergesortcE_in_gaa(x1, x2, x3)  =  mergesortcE_in_gaa(x1)
mergesortcE_out_gaa(x1, x2, x3)  =  mergesortcE_out_gaa(x1, x2)
U38_gaa(x1, x2, x3, x4, x5, x6, x7)  =  U38_gaa(x1, x2, x3, x7)
U39_gaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  U39_gaa(x1, x2, x3, x7, x8)
U40_gaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  U40_gaa(x1, x2, x3, x7, x8)
U41_gaa(x1, x2, x3, x4, x5, x6, x7)  =  U41_gaa(x1, x2, x3, x7)
mergecC_in_ggaaa(x1, x2, x3, x4, x5)  =  mergecC_in_ggaaa(x1, x2)
mergecC_out_ggaaa(x1, x2, x3, x4, x5)  =  mergecC_out_ggaaa(x1, x2, x3)
U42_ggaaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  U42_ggaaa(x1, x2, x3, x4, x8)
qcF_in_ggggaa(x1, x2, x3, x4, x5, x6)  =  qcF_in_ggggaa(x1, x2, x3, x4)
U45_ggggaa(x1, x2, x3, x4, x5)  =  U45_ggggaa(x1, x2, x3, x5)
lecH_in_gg(x1, x2)  =  lecH_in_gg(x1, x2)
s(x1)  =  s(x1)
U44_gg(x1, x2, x3)  =  U44_gg(x1, x2, x3)
0  =  0
lecH_out_gg(x1, x2)  =  lecH_out_gg(x1, x2)
qcF_out_ggggaa(x1, x2, x3, x4, x5, x6)  =  qcF_out_ggggaa(x1, x2, x3, x4, x5)
U46_ggggaa(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U46_ggggaa(x1, x2, x3, x4, x5, x9)
U47_ggggaa(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U47_ggggaa(x1, x2, x3, x4, x5, x9)
U48_ggggaa(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U48_ggggaa(x1, x2, x3, x4, x5, x9)
U49_ggggaa(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U49_ggggaa(x1, x2, x3, x4, x5, x9)
qcG_in_ggggaa(x1, x2, x3, x4, x5, x6)  =  qcG_in_ggggaa(x1, x2, x3, x4)
U51_ggggaa(x1, x2, x3, x4, x5)  =  U51_ggggaa(x1, x2, x3, x5)
gtcI_in_gg(x1, x2)  =  gtcI_in_gg(x1, x2)
U50_gg(x1, x2, x3)  =  U50_gg(x1, x2, x3)
gtcI_out_gg(x1, x2)  =  gtcI_out_gg(x1, x2)
qcG_out_ggggaa(x1, x2, x3, x4, x5, x6)  =  qcG_out_ggggaa(x1, x2, x3, x4, x5)
U52_ggggaa(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U52_ggggaa(x1, x2, x3, x4, x5, x9)
U53_ggggaa(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U53_ggggaa(x1, x2, x3, x4, x5, x9)
U54_ggggaa(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U54_ggggaa(x1, x2, x3, x4, x5, x9)
U55_ggggaa(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U55_ggggaa(x1, x2, x3, x4, x5, x9)
U43_ggaaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  U43_ggaaa(x1, x2, x3, x4, x8)
U36_gaa(x1, x2, x3, x4, x5, x6, x7)  =  U36_gaa(x1, x2, x3, x7)
SPLITA_IN_GAAA(x1, x2, x3, x4)  =  SPLITA_IN_GAAA(x1)

We have to consider all (P,R,Pi)-chains

(29) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(30) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

SPLITA_IN_GAAA(.(X1, X2), .(X1, X3), X4, .(X5, X6)) → SPLITA_IN_GAAA(X2, X4, X3, X6)

R is empty.
The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x1, x2)
SPLITA_IN_GAAA(x1, x2, x3, x4)  =  SPLITA_IN_GAAA(x1)

We have to consider all (P,R,Pi)-chains

(31) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(32) Obligation:

Q DP problem:
The TRS P consists of the following rules:

SPLITA_IN_GAAA(.(X1, X2)) → SPLITA_IN_GAAA(X2)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(33) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

  • SPLITA_IN_GAAA(.(X1, X2)) → SPLITA_IN_GAAA(X2)
    The graph contains the following edges 1 > 1

(34) YES

(35) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

MERGESORTE_IN_GAA(.(X1, .(X2, X3)), X4, .(X5, X6)) → U4_GAA(X1, X2, X3, X4, X5, X6, splitcD_in_ggaaa(X1, .(X2, X3), X7, X8, .(X5, X6)))
U4_GAA(X1, X2, X3, X4, X5, X6, splitcD_out_ggaaa(X1, .(X2, X3), X7, X8, .(X5, X6))) → MERGESORTE_IN_GAA(X7, X9, X6)
U4_GAA(X1, X2, X3, X4, X5, X6, splitcD_out_ggaaa(X1, .(X2, X3), X7, X8, .(X5, X6))) → U6_GAA(X1, X2, X3, X4, X5, X6, X8, mergesortcE_in_gaa(X7, X9, X6))
U6_GAA(X1, X2, X3, X4, X5, X6, X8, mergesortcE_out_gaa(X7, X9, X6)) → MERGESORTE_IN_GAA(X8, X10, X6)

The TRS R consists of the following rules:

splitcD_in_ggaaa(X1, X2, .(X1, X3), X4, .(X5, X6)) → U37_ggaaa(X1, X2, X3, X4, X5, X6, splitcA_in_gaaa(X2, X4, X3, X6))
splitcA_in_gaaa([], [], [], X1) → splitcA_out_gaaa([], [], [], X1)
splitcA_in_gaaa(.(X1, X2), .(X1, X3), X4, .(X5, X6)) → U32_gaaa(X1, X2, X3, X4, X5, X6, splitcA_in_gaaa(X2, X4, X3, X6))
U32_gaaa(X1, X2, X3, X4, X5, X6, splitcA_out_gaaa(X2, X4, X3, X6)) → splitcA_out_gaaa(.(X1, X2), .(X1, X3), X4, .(X5, X6))
U37_ggaaa(X1, X2, X3, X4, X5, X6, splitcA_out_gaaa(X2, X4, X3, X6)) → splitcD_out_ggaaa(X1, X2, .(X1, X3), X4, .(X5, X6))
mergesortcB_in_gaa([], [], X1) → mergesortcB_out_gaa([], [], X1)
mergesortcB_in_gaa(.(X1, []), .(X1, []), X2) → mergesortcB_out_gaa(.(X1, []), .(X1, []), X2)
mergesortcB_in_gaa(.(X1, .(X2, X3)), X4, .(X5, X6)) → U33_gaa(X1, X2, X3, X4, X5, X6, splitcD_in_ggaaa(X2, X3, X7, X8, X6))
U33_gaa(X1, X2, X3, X4, X5, X6, splitcD_out_ggaaa(X2, X3, X7, X8, X6)) → U34_gaa(X1, X2, X3, X4, X5, X6, X7, mergesortcB_in_gaa(.(X1, X8), X9, X6))
U34_gaa(X1, X2, X3, X4, X5, X6, X7, mergesortcB_out_gaa(.(X1, X8), X9, X6)) → U35_gaa(X1, X2, X3, X4, X5, X6, X9, mergesortcE_in_gaa(X7, X10, X6))
mergesortcE_in_gaa([], [], X1) → mergesortcE_out_gaa([], [], X1)
mergesortcE_in_gaa(.(X1, []), .(X1, []), X2) → mergesortcE_out_gaa(.(X1, []), .(X1, []), X2)
mergesortcE_in_gaa(.(X1, .(X2, X3)), X4, .(X5, X6)) → U38_gaa(X1, X2, X3, X4, X5, X6, splitcD_in_ggaaa(X1, .(X2, X3), X7, X8, .(X5, X6)))
U38_gaa(X1, X2, X3, X4, X5, X6, splitcD_out_ggaaa(X1, .(X2, X3), X7, X8, .(X5, X6))) → U39_gaa(X1, X2, X3, X4, X5, X6, X8, mergesortcE_in_gaa(X7, X9, X6))
U39_gaa(X1, X2, X3, X4, X5, X6, X8, mergesortcE_out_gaa(X7, X9, X6)) → U40_gaa(X1, X2, X3, X4, X5, X6, X9, mergesortcE_in_gaa(X8, X10, X6))
U40_gaa(X1, X2, X3, X4, X5, X6, X9, mergesortcE_out_gaa(X8, X10, X6)) → U41_gaa(X1, X2, X3, X4, X5, X6, mergecC_in_ggaaa(X9, X10, X4, X5, X6))
mergecC_in_ggaaa([], X1, X1, X2, X3) → mergecC_out_ggaaa([], X1, X1, X2, X3)
mergecC_in_ggaaa(X1, [], X1, X2, X3) → mergecC_out_ggaaa(X1, [], X1, X2, X3)
mergecC_in_ggaaa(.(X1, X2), .(X3, X4), .(X1, X5), X6, X7) → U42_ggaaa(X1, X2, X3, X4, X5, X6, X7, qcF_in_ggggaa(X1, X3, X2, X4, X5, X7))
qcF_in_ggggaa(X1, X2, [], X3, .(X2, X3), X4) → U45_ggggaa(X1, X2, X3, X4, lecH_in_gg(X1, X2))
lecH_in_gg(s(X1), s(X2)) → U44_gg(X1, X2, lecH_in_gg(X1, X2))
lecH_in_gg(0, s(0)) → lecH_out_gg(0, s(0))
lecH_in_gg(0, 0) → lecH_out_gg(0, 0)
U44_gg(X1, X2, lecH_out_gg(X1, X2)) → lecH_out_gg(s(X1), s(X2))
U45_ggggaa(X1, X2, X3, X4, lecH_out_gg(X1, X2)) → qcF_out_ggggaa(X1, X2, [], X3, .(X2, X3), X4)
qcF_in_ggggaa(X1, X2, .(X3, X4), X5, .(X3, X6), .(X7, X8)) → U46_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, lecH_in_gg(X1, X2))
U46_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, lecH_out_gg(X1, X2)) → U47_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, qcF_in_ggggaa(X3, X2, X4, X5, X6, X8))
qcF_in_ggggaa(X1, X2, .(X3, X4), X5, .(X2, X6), .(X7, X8)) → U48_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, lecH_in_gg(X1, X2))
U48_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, lecH_out_gg(X1, X2)) → U49_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, qcG_in_ggggaa(X3, X2, X4, X5, X6, X8))
qcG_in_ggggaa(X1, X2, X3, [], .(X1, X3), X4) → U51_ggggaa(X1, X2, X3, X4, gtcI_in_gg(X1, X2))
gtcI_in_gg(s(X1), s(X2)) → U50_gg(X1, X2, gtcI_in_gg(X1, X2))
gtcI_in_gg(s(0), 0) → gtcI_out_gg(s(0), 0)
U50_gg(X1, X2, gtcI_out_gg(X1, X2)) → gtcI_out_gg(s(X1), s(X2))
U51_ggggaa(X1, X2, X3, X4, gtcI_out_gg(X1, X2)) → qcG_out_ggggaa(X1, X2, X3, [], .(X1, X3), X4)
qcG_in_ggggaa(X1, X2, X3, .(X4, X5), .(X1, X6), .(X7, X8)) → U52_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, gtcI_in_gg(X1, X2))
U52_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, gtcI_out_gg(X1, X2)) → U53_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, qcF_in_ggggaa(X1, X4, X3, X5, X6, X8))
U53_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, qcF_out_ggggaa(X1, X4, X3, X5, X6, X8)) → qcG_out_ggggaa(X1, X2, X3, .(X4, X5), .(X1, X6), .(X7, X8))
qcG_in_ggggaa(X1, X2, X3, .(X4, X5), .(X4, X6), .(X7, X8)) → U54_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, gtcI_in_gg(X1, X2))
U54_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, gtcI_out_gg(X1, X2)) → U55_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, qcG_in_ggggaa(X1, X4, X3, X5, X6, X8))
U55_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, qcG_out_ggggaa(X1, X4, X3, X5, X6, X8)) → qcG_out_ggggaa(X1, X2, X3, .(X4, X5), .(X4, X6), .(X7, X8))
U49_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, qcG_out_ggggaa(X3, X2, X4, X5, X6, X8)) → qcF_out_ggggaa(X1, X2, .(X3, X4), X5, .(X2, X6), .(X7, X8))
U47_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, qcF_out_ggggaa(X3, X2, X4, X5, X6, X8)) → qcF_out_ggggaa(X1, X2, .(X3, X4), X5, .(X3, X6), .(X7, X8))
U42_ggaaa(X1, X2, X3, X4, X5, X6, X7, qcF_out_ggggaa(X1, X3, X2, X4, X5, X7)) → mergecC_out_ggaaa(.(X1, X2), .(X3, X4), .(X1, X5), X6, X7)
mergecC_in_ggaaa(.(X1, X2), .(X3, X4), .(X3, X5), X6, X7) → U43_ggaaa(X1, X2, X3, X4, X5, X6, X7, qcG_in_ggggaa(X1, X3, X2, X4, X5, X7))
U43_ggaaa(X1, X2, X3, X4, X5, X6, X7, qcG_out_ggggaa(X1, X3, X2, X4, X5, X7)) → mergecC_out_ggaaa(.(X1, X2), .(X3, X4), .(X3, X5), X6, X7)
U41_gaa(X1, X2, X3, X4, X5, X6, mergecC_out_ggaaa(X9, X10, X4, X5, X6)) → mergesortcE_out_gaa(.(X1, .(X2, X3)), X4, .(X5, X6))
U35_gaa(X1, X2, X3, X4, X5, X6, X9, mergesortcE_out_gaa(X7, X10, X6)) → U36_gaa(X1, X2, X3, X4, X5, X6, mergecC_in_ggaaa(X9, X10, X4, X5, X6))
U36_gaa(X1, X2, X3, X4, X5, X6, mergecC_out_ggaaa(X9, X10, X4, X5, X6)) → mergesortcB_out_gaa(.(X1, .(X2, X3)), X4, .(X5, X6))

The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x1, x2)
splitcD_in_ggaaa(x1, x2, x3, x4, x5)  =  splitcD_in_ggaaa(x1, x2)
U37_ggaaa(x1, x2, x3, x4, x5, x6, x7)  =  U37_ggaaa(x1, x2, x7)
splitcA_in_gaaa(x1, x2, x3, x4)  =  splitcA_in_gaaa(x1)
[]  =  []
splitcA_out_gaaa(x1, x2, x3, x4)  =  splitcA_out_gaaa(x1, x2, x3)
U32_gaaa(x1, x2, x3, x4, x5, x6, x7)  =  U32_gaaa(x1, x2, x7)
splitcD_out_ggaaa(x1, x2, x3, x4, x5)  =  splitcD_out_ggaaa(x1, x2, x3, x4)
mergesortcB_in_gaa(x1, x2, x3)  =  mergesortcB_in_gaa(x1)
mergesortcB_out_gaa(x1, x2, x3)  =  mergesortcB_out_gaa(x1, x2)
U33_gaa(x1, x2, x3, x4, x5, x6, x7)  =  U33_gaa(x1, x2, x3, x7)
U34_gaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  U34_gaa(x1, x2, x3, x7, x8)
U35_gaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  U35_gaa(x1, x2, x3, x7, x8)
mergesortcE_in_gaa(x1, x2, x3)  =  mergesortcE_in_gaa(x1)
mergesortcE_out_gaa(x1, x2, x3)  =  mergesortcE_out_gaa(x1, x2)
U38_gaa(x1, x2, x3, x4, x5, x6, x7)  =  U38_gaa(x1, x2, x3, x7)
U39_gaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  U39_gaa(x1, x2, x3, x7, x8)
U40_gaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  U40_gaa(x1, x2, x3, x7, x8)
U41_gaa(x1, x2, x3, x4, x5, x6, x7)  =  U41_gaa(x1, x2, x3, x7)
mergecC_in_ggaaa(x1, x2, x3, x4, x5)  =  mergecC_in_ggaaa(x1, x2)
mergecC_out_ggaaa(x1, x2, x3, x4, x5)  =  mergecC_out_ggaaa(x1, x2, x3)
U42_ggaaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  U42_ggaaa(x1, x2, x3, x4, x8)
qcF_in_ggggaa(x1, x2, x3, x4, x5, x6)  =  qcF_in_ggggaa(x1, x2, x3, x4)
U45_ggggaa(x1, x2, x3, x4, x5)  =  U45_ggggaa(x1, x2, x3, x5)
lecH_in_gg(x1, x2)  =  lecH_in_gg(x1, x2)
s(x1)  =  s(x1)
U44_gg(x1, x2, x3)  =  U44_gg(x1, x2, x3)
0  =  0
lecH_out_gg(x1, x2)  =  lecH_out_gg(x1, x2)
qcF_out_ggggaa(x1, x2, x3, x4, x5, x6)  =  qcF_out_ggggaa(x1, x2, x3, x4, x5)
U46_ggggaa(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U46_ggggaa(x1, x2, x3, x4, x5, x9)
U47_ggggaa(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U47_ggggaa(x1, x2, x3, x4, x5, x9)
U48_ggggaa(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U48_ggggaa(x1, x2, x3, x4, x5, x9)
U49_ggggaa(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U49_ggggaa(x1, x2, x3, x4, x5, x9)
qcG_in_ggggaa(x1, x2, x3, x4, x5, x6)  =  qcG_in_ggggaa(x1, x2, x3, x4)
U51_ggggaa(x1, x2, x3, x4, x5)  =  U51_ggggaa(x1, x2, x3, x5)
gtcI_in_gg(x1, x2)  =  gtcI_in_gg(x1, x2)
U50_gg(x1, x2, x3)  =  U50_gg(x1, x2, x3)
gtcI_out_gg(x1, x2)  =  gtcI_out_gg(x1, x2)
qcG_out_ggggaa(x1, x2, x3, x4, x5, x6)  =  qcG_out_ggggaa(x1, x2, x3, x4, x5)
U52_ggggaa(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U52_ggggaa(x1, x2, x3, x4, x5, x9)
U53_ggggaa(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U53_ggggaa(x1, x2, x3, x4, x5, x9)
U54_ggggaa(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U54_ggggaa(x1, x2, x3, x4, x5, x9)
U55_ggggaa(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U55_ggggaa(x1, x2, x3, x4, x5, x9)
U43_ggaaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  U43_ggaaa(x1, x2, x3, x4, x8)
U36_gaa(x1, x2, x3, x4, x5, x6, x7)  =  U36_gaa(x1, x2, x3, x7)
MERGESORTE_IN_GAA(x1, x2, x3)  =  MERGESORTE_IN_GAA(x1)
U4_GAA(x1, x2, x3, x4, x5, x6, x7)  =  U4_GAA(x1, x2, x3, x7)
U6_GAA(x1, x2, x3, x4, x5, x6, x7, x8)  =  U6_GAA(x1, x2, x3, x7, x8)

We have to consider all (P,R,Pi)-chains

(36) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(37) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

MERGESORTE_IN_GAA(.(X1, .(X2, X3)), X4, .(X5, X6)) → U4_GAA(X1, X2, X3, X4, X5, X6, splitcD_in_ggaaa(X1, .(X2, X3), X7, X8, .(X5, X6)))
U4_GAA(X1, X2, X3, X4, X5, X6, splitcD_out_ggaaa(X1, .(X2, X3), X7, X8, .(X5, X6))) → MERGESORTE_IN_GAA(X7, X9, X6)
U4_GAA(X1, X2, X3, X4, X5, X6, splitcD_out_ggaaa(X1, .(X2, X3), X7, X8, .(X5, X6))) → U6_GAA(X1, X2, X3, X4, X5, X6, X8, mergesortcE_in_gaa(X7, X9, X6))
U6_GAA(X1, X2, X3, X4, X5, X6, X8, mergesortcE_out_gaa(X7, X9, X6)) → MERGESORTE_IN_GAA(X8, X10, X6)

The TRS R consists of the following rules:

splitcD_in_ggaaa(X1, X2, .(X1, X3), X4, .(X5, X6)) → U37_ggaaa(X1, X2, X3, X4, X5, X6, splitcA_in_gaaa(X2, X4, X3, X6))
mergesortcE_in_gaa([], [], X1) → mergesortcE_out_gaa([], [], X1)
mergesortcE_in_gaa(.(X1, []), .(X1, []), X2) → mergesortcE_out_gaa(.(X1, []), .(X1, []), X2)
mergesortcE_in_gaa(.(X1, .(X2, X3)), X4, .(X5, X6)) → U38_gaa(X1, X2, X3, X4, X5, X6, splitcD_in_ggaaa(X1, .(X2, X3), X7, X8, .(X5, X6)))
U37_ggaaa(X1, X2, X3, X4, X5, X6, splitcA_out_gaaa(X2, X4, X3, X6)) → splitcD_out_ggaaa(X1, X2, .(X1, X3), X4, .(X5, X6))
U38_gaa(X1, X2, X3, X4, X5, X6, splitcD_out_ggaaa(X1, .(X2, X3), X7, X8, .(X5, X6))) → U39_gaa(X1, X2, X3, X4, X5, X6, X8, mergesortcE_in_gaa(X7, X9, X6))
splitcA_in_gaaa([], [], [], X1) → splitcA_out_gaaa([], [], [], X1)
splitcA_in_gaaa(.(X1, X2), .(X1, X3), X4, .(X5, X6)) → U32_gaaa(X1, X2, X3, X4, X5, X6, splitcA_in_gaaa(X2, X4, X3, X6))
U39_gaa(X1, X2, X3, X4, X5, X6, X8, mergesortcE_out_gaa(X7, X9, X6)) → U40_gaa(X1, X2, X3, X4, X5, X6, X9, mergesortcE_in_gaa(X8, X10, X6))
U32_gaaa(X1, X2, X3, X4, X5, X6, splitcA_out_gaaa(X2, X4, X3, X6)) → splitcA_out_gaaa(.(X1, X2), .(X1, X3), X4, .(X5, X6))
U40_gaa(X1, X2, X3, X4, X5, X6, X9, mergesortcE_out_gaa(X8, X10, X6)) → U41_gaa(X1, X2, X3, X4, X5, X6, mergecC_in_ggaaa(X9, X10, X4, X5, X6))
U41_gaa(X1, X2, X3, X4, X5, X6, mergecC_out_ggaaa(X9, X10, X4, X5, X6)) → mergesortcE_out_gaa(.(X1, .(X2, X3)), X4, .(X5, X6))
mergecC_in_ggaaa([], X1, X1, X2, X3) → mergecC_out_ggaaa([], X1, X1, X2, X3)
mergecC_in_ggaaa(X1, [], X1, X2, X3) → mergecC_out_ggaaa(X1, [], X1, X2, X3)
mergecC_in_ggaaa(.(X1, X2), .(X3, X4), .(X1, X5), X6, X7) → U42_ggaaa(X1, X2, X3, X4, X5, X6, X7, qcF_in_ggggaa(X1, X3, X2, X4, X5, X7))
mergecC_in_ggaaa(.(X1, X2), .(X3, X4), .(X3, X5), X6, X7) → U43_ggaaa(X1, X2, X3, X4, X5, X6, X7, qcG_in_ggggaa(X1, X3, X2, X4, X5, X7))
U42_ggaaa(X1, X2, X3, X4, X5, X6, X7, qcF_out_ggggaa(X1, X3, X2, X4, X5, X7)) → mergecC_out_ggaaa(.(X1, X2), .(X3, X4), .(X1, X5), X6, X7)
U43_ggaaa(X1, X2, X3, X4, X5, X6, X7, qcG_out_ggggaa(X1, X3, X2, X4, X5, X7)) → mergecC_out_ggaaa(.(X1, X2), .(X3, X4), .(X3, X5), X6, X7)
qcF_in_ggggaa(X1, X2, [], X3, .(X2, X3), X4) → U45_ggggaa(X1, X2, X3, X4, lecH_in_gg(X1, X2))
qcF_in_ggggaa(X1, X2, .(X3, X4), X5, .(X3, X6), .(X7, X8)) → U46_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, lecH_in_gg(X1, X2))
qcF_in_ggggaa(X1, X2, .(X3, X4), X5, .(X2, X6), .(X7, X8)) → U48_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, lecH_in_gg(X1, X2))
qcG_in_ggggaa(X1, X2, X3, [], .(X1, X3), X4) → U51_ggggaa(X1, X2, X3, X4, gtcI_in_gg(X1, X2))
qcG_in_ggggaa(X1, X2, X3, .(X4, X5), .(X1, X6), .(X7, X8)) → U52_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, gtcI_in_gg(X1, X2))
qcG_in_ggggaa(X1, X2, X3, .(X4, X5), .(X4, X6), .(X7, X8)) → U54_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, gtcI_in_gg(X1, X2))
U45_ggggaa(X1, X2, X3, X4, lecH_out_gg(X1, X2)) → qcF_out_ggggaa(X1, X2, [], X3, .(X2, X3), X4)
U46_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, lecH_out_gg(X1, X2)) → U47_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, qcF_in_ggggaa(X3, X2, X4, X5, X6, X8))
U48_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, lecH_out_gg(X1, X2)) → U49_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, qcG_in_ggggaa(X3, X2, X4, X5, X6, X8))
U51_ggggaa(X1, X2, X3, X4, gtcI_out_gg(X1, X2)) → qcG_out_ggggaa(X1, X2, X3, [], .(X1, X3), X4)
U52_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, gtcI_out_gg(X1, X2)) → U53_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, qcF_in_ggggaa(X1, X4, X3, X5, X6, X8))
U54_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, gtcI_out_gg(X1, X2)) → U55_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, qcG_in_ggggaa(X1, X4, X3, X5, X6, X8))
lecH_in_gg(s(X1), s(X2)) → U44_gg(X1, X2, lecH_in_gg(X1, X2))
lecH_in_gg(0, s(0)) → lecH_out_gg(0, s(0))
lecH_in_gg(0, 0) → lecH_out_gg(0, 0)
U47_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, qcF_out_ggggaa(X3, X2, X4, X5, X6, X8)) → qcF_out_ggggaa(X1, X2, .(X3, X4), X5, .(X3, X6), .(X7, X8))
U49_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, qcG_out_ggggaa(X3, X2, X4, X5, X6, X8)) → qcF_out_ggggaa(X1, X2, .(X3, X4), X5, .(X2, X6), .(X7, X8))
gtcI_in_gg(s(X1), s(X2)) → U50_gg(X1, X2, gtcI_in_gg(X1, X2))
gtcI_in_gg(s(0), 0) → gtcI_out_gg(s(0), 0)
U53_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, qcF_out_ggggaa(X1, X4, X3, X5, X6, X8)) → qcG_out_ggggaa(X1, X2, X3, .(X4, X5), .(X1, X6), .(X7, X8))
U55_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, qcG_out_ggggaa(X1, X4, X3, X5, X6, X8)) → qcG_out_ggggaa(X1, X2, X3, .(X4, X5), .(X4, X6), .(X7, X8))
U44_gg(X1, X2, lecH_out_gg(X1, X2)) → lecH_out_gg(s(X1), s(X2))
U50_gg(X1, X2, gtcI_out_gg(X1, X2)) → gtcI_out_gg(s(X1), s(X2))

The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x1, x2)
splitcD_in_ggaaa(x1, x2, x3, x4, x5)  =  splitcD_in_ggaaa(x1, x2)
U37_ggaaa(x1, x2, x3, x4, x5, x6, x7)  =  U37_ggaaa(x1, x2, x7)
splitcA_in_gaaa(x1, x2, x3, x4)  =  splitcA_in_gaaa(x1)
[]  =  []
splitcA_out_gaaa(x1, x2, x3, x4)  =  splitcA_out_gaaa(x1, x2, x3)
U32_gaaa(x1, x2, x3, x4, x5, x6, x7)  =  U32_gaaa(x1, x2, x7)
splitcD_out_ggaaa(x1, x2, x3, x4, x5)  =  splitcD_out_ggaaa(x1, x2, x3, x4)
mergesortcE_in_gaa(x1, x2, x3)  =  mergesortcE_in_gaa(x1)
mergesortcE_out_gaa(x1, x2, x3)  =  mergesortcE_out_gaa(x1, x2)
U38_gaa(x1, x2, x3, x4, x5, x6, x7)  =  U38_gaa(x1, x2, x3, x7)
U39_gaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  U39_gaa(x1, x2, x3, x7, x8)
U40_gaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  U40_gaa(x1, x2, x3, x7, x8)
U41_gaa(x1, x2, x3, x4, x5, x6, x7)  =  U41_gaa(x1, x2, x3, x7)
mergecC_in_ggaaa(x1, x2, x3, x4, x5)  =  mergecC_in_ggaaa(x1, x2)
mergecC_out_ggaaa(x1, x2, x3, x4, x5)  =  mergecC_out_ggaaa(x1, x2, x3)
U42_ggaaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  U42_ggaaa(x1, x2, x3, x4, x8)
qcF_in_ggggaa(x1, x2, x3, x4, x5, x6)  =  qcF_in_ggggaa(x1, x2, x3, x4)
U45_ggggaa(x1, x2, x3, x4, x5)  =  U45_ggggaa(x1, x2, x3, x5)
lecH_in_gg(x1, x2)  =  lecH_in_gg(x1, x2)
s(x1)  =  s(x1)
U44_gg(x1, x2, x3)  =  U44_gg(x1, x2, x3)
0  =  0
lecH_out_gg(x1, x2)  =  lecH_out_gg(x1, x2)
qcF_out_ggggaa(x1, x2, x3, x4, x5, x6)  =  qcF_out_ggggaa(x1, x2, x3, x4, x5)
U46_ggggaa(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U46_ggggaa(x1, x2, x3, x4, x5, x9)
U47_ggggaa(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U47_ggggaa(x1, x2, x3, x4, x5, x9)
U48_ggggaa(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U48_ggggaa(x1, x2, x3, x4, x5, x9)
U49_ggggaa(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U49_ggggaa(x1, x2, x3, x4, x5, x9)
qcG_in_ggggaa(x1, x2, x3, x4, x5, x6)  =  qcG_in_ggggaa(x1, x2, x3, x4)
U51_ggggaa(x1, x2, x3, x4, x5)  =  U51_ggggaa(x1, x2, x3, x5)
gtcI_in_gg(x1, x2)  =  gtcI_in_gg(x1, x2)
U50_gg(x1, x2, x3)  =  U50_gg(x1, x2, x3)
gtcI_out_gg(x1, x2)  =  gtcI_out_gg(x1, x2)
qcG_out_ggggaa(x1, x2, x3, x4, x5, x6)  =  qcG_out_ggggaa(x1, x2, x3, x4, x5)
U52_ggggaa(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U52_ggggaa(x1, x2, x3, x4, x5, x9)
U53_ggggaa(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U53_ggggaa(x1, x2, x3, x4, x5, x9)
U54_ggggaa(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U54_ggggaa(x1, x2, x3, x4, x5, x9)
U55_ggggaa(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U55_ggggaa(x1, x2, x3, x4, x5, x9)
U43_ggaaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  U43_ggaaa(x1, x2, x3, x4, x8)
MERGESORTE_IN_GAA(x1, x2, x3)  =  MERGESORTE_IN_GAA(x1)
U4_GAA(x1, x2, x3, x4, x5, x6, x7)  =  U4_GAA(x1, x2, x3, x7)
U6_GAA(x1, x2, x3, x4, x5, x6, x7, x8)  =  U6_GAA(x1, x2, x3, x7, x8)

We have to consider all (P,R,Pi)-chains

(38) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(39) Obligation:

Q DP problem:
The TRS P consists of the following rules:

MERGESORTE_IN_GAA(.(X1, .(X2, X3))) → U4_GAA(X1, X2, X3, splitcD_in_ggaaa(X1, .(X2, X3)))
U4_GAA(X1, X2, X3, splitcD_out_ggaaa(X1, .(X2, X3), X7, X8)) → MERGESORTE_IN_GAA(X7)
U4_GAA(X1, X2, X3, splitcD_out_ggaaa(X1, .(X2, X3), X7, X8)) → U6_GAA(X1, X2, X3, X8, mergesortcE_in_gaa(X7))
U6_GAA(X1, X2, X3, X8, mergesortcE_out_gaa(X7, X9)) → MERGESORTE_IN_GAA(X8)

The TRS R consists of the following rules:

splitcD_in_ggaaa(X1, X2) → U37_ggaaa(X1, X2, splitcA_in_gaaa(X2))
mergesortcE_in_gaa([]) → mergesortcE_out_gaa([], [])
mergesortcE_in_gaa(.(X1, [])) → mergesortcE_out_gaa(.(X1, []), .(X1, []))
mergesortcE_in_gaa(.(X1, .(X2, X3))) → U38_gaa(X1, X2, X3, splitcD_in_ggaaa(X1, .(X2, X3)))
U37_ggaaa(X1, X2, splitcA_out_gaaa(X2, X4, X3)) → splitcD_out_ggaaa(X1, X2, .(X1, X3), X4)
U38_gaa(X1, X2, X3, splitcD_out_ggaaa(X1, .(X2, X3), X7, X8)) → U39_gaa(X1, X2, X3, X8, mergesortcE_in_gaa(X7))
splitcA_in_gaaa([]) → splitcA_out_gaaa([], [], [])
splitcA_in_gaaa(.(X1, X2)) → U32_gaaa(X1, X2, splitcA_in_gaaa(X2))
U39_gaa(X1, X2, X3, X8, mergesortcE_out_gaa(X7, X9)) → U40_gaa(X1, X2, X3, X9, mergesortcE_in_gaa(X8))
U32_gaaa(X1, X2, splitcA_out_gaaa(X2, X4, X3)) → splitcA_out_gaaa(.(X1, X2), .(X1, X3), X4)
U40_gaa(X1, X2, X3, X9, mergesortcE_out_gaa(X8, X10)) → U41_gaa(X1, X2, X3, mergecC_in_ggaaa(X9, X10))
U41_gaa(X1, X2, X3, mergecC_out_ggaaa(X9, X10, X4)) → mergesortcE_out_gaa(.(X1, .(X2, X3)), X4)
mergecC_in_ggaaa([], X1) → mergecC_out_ggaaa([], X1, X1)
mergecC_in_ggaaa(X1, []) → mergecC_out_ggaaa(X1, [], X1)
mergecC_in_ggaaa(.(X1, X2), .(X3, X4)) → U42_ggaaa(X1, X2, X3, X4, qcF_in_ggggaa(X1, X3, X2, X4))
mergecC_in_ggaaa(.(X1, X2), .(X3, X4)) → U43_ggaaa(X1, X2, X3, X4, qcG_in_ggggaa(X1, X3, X2, X4))
U42_ggaaa(X1, X2, X3, X4, qcF_out_ggggaa(X1, X3, X2, X4, X5)) → mergecC_out_ggaaa(.(X1, X2), .(X3, X4), .(X1, X5))
U43_ggaaa(X1, X2, X3, X4, qcG_out_ggggaa(X1, X3, X2, X4, X5)) → mergecC_out_ggaaa(.(X1, X2), .(X3, X4), .(X3, X5))
qcF_in_ggggaa(X1, X2, [], X3) → U45_ggggaa(X1, X2, X3, lecH_in_gg(X1, X2))
qcF_in_ggggaa(X1, X2, .(X3, X4), X5) → U46_ggggaa(X1, X2, X3, X4, X5, lecH_in_gg(X1, X2))
qcF_in_ggggaa(X1, X2, .(X3, X4), X5) → U48_ggggaa(X1, X2, X3, X4, X5, lecH_in_gg(X1, X2))
qcG_in_ggggaa(X1, X2, X3, []) → U51_ggggaa(X1, X2, X3, gtcI_in_gg(X1, X2))
qcG_in_ggggaa(X1, X2, X3, .(X4, X5)) → U52_ggggaa(X1, X2, X3, X4, X5, gtcI_in_gg(X1, X2))
qcG_in_ggggaa(X1, X2, X3, .(X4, X5)) → U54_ggggaa(X1, X2, X3, X4, X5, gtcI_in_gg(X1, X2))
U45_ggggaa(X1, X2, X3, lecH_out_gg(X1, X2)) → qcF_out_ggggaa(X1, X2, [], X3, .(X2, X3))
U46_ggggaa(X1, X2, X3, X4, X5, lecH_out_gg(X1, X2)) → U47_ggggaa(X1, X2, X3, X4, X5, qcF_in_ggggaa(X3, X2, X4, X5))
U48_ggggaa(X1, X2, X3, X4, X5, lecH_out_gg(X1, X2)) → U49_ggggaa(X1, X2, X3, X4, X5, qcG_in_ggggaa(X3, X2, X4, X5))
U51_ggggaa(X1, X2, X3, gtcI_out_gg(X1, X2)) → qcG_out_ggggaa(X1, X2, X3, [], .(X1, X3))
U52_ggggaa(X1, X2, X3, X4, X5, gtcI_out_gg(X1, X2)) → U53_ggggaa(X1, X2, X3, X4, X5, qcF_in_ggggaa(X1, X4, X3, X5))
U54_ggggaa(X1, X2, X3, X4, X5, gtcI_out_gg(X1, X2)) → U55_ggggaa(X1, X2, X3, X4, X5, qcG_in_ggggaa(X1, X4, X3, X5))
lecH_in_gg(s(X1), s(X2)) → U44_gg(X1, X2, lecH_in_gg(X1, X2))
lecH_in_gg(0, s(0)) → lecH_out_gg(0, s(0))
lecH_in_gg(0, 0) → lecH_out_gg(0, 0)
U47_ggggaa(X1, X2, X3, X4, X5, qcF_out_ggggaa(X3, X2, X4, X5, X6)) → qcF_out_ggggaa(X1, X2, .(X3, X4), X5, .(X3, X6))
U49_ggggaa(X1, X2, X3, X4, X5, qcG_out_ggggaa(X3, X2, X4, X5, X6)) → qcF_out_ggggaa(X1, X2, .(X3, X4), X5, .(X2, X6))
gtcI_in_gg(s(X1), s(X2)) → U50_gg(X1, X2, gtcI_in_gg(X1, X2))
gtcI_in_gg(s(0), 0) → gtcI_out_gg(s(0), 0)
U53_ggggaa(X1, X2, X3, X4, X5, qcF_out_ggggaa(X1, X4, X3, X5, X6)) → qcG_out_ggggaa(X1, X2, X3, .(X4, X5), .(X1, X6))
U55_ggggaa(X1, X2, X3, X4, X5, qcG_out_ggggaa(X1, X4, X3, X5, X6)) → qcG_out_ggggaa(X1, X2, X3, .(X4, X5), .(X4, X6))
U44_gg(X1, X2, lecH_out_gg(X1, X2)) → lecH_out_gg(s(X1), s(X2))
U50_gg(X1, X2, gtcI_out_gg(X1, X2)) → gtcI_out_gg(s(X1), s(X2))

The set Q consists of the following terms:

splitcD_in_ggaaa(x0, x1)
mergesortcE_in_gaa(x0)
U37_ggaaa(x0, x1, x2)
U38_gaa(x0, x1, x2, x3)
splitcA_in_gaaa(x0)
U39_gaa(x0, x1, x2, x3, x4)
U32_gaaa(x0, x1, x2)
U40_gaa(x0, x1, x2, x3, x4)
U41_gaa(x0, x1, x2, x3)
mergecC_in_ggaaa(x0, x1)
U42_ggaaa(x0, x1, x2, x3, x4)
U43_ggaaa(x0, x1, x2, x3, x4)
qcF_in_ggggaa(x0, x1, x2, x3)
qcG_in_ggggaa(x0, x1, x2, x3)
U45_ggggaa(x0, x1, x2, x3)
U46_ggggaa(x0, x1, x2, x3, x4, x5)
U48_ggggaa(x0, x1, x2, x3, x4, x5)
U51_ggggaa(x0, x1, x2, x3)
U52_ggggaa(x0, x1, x2, x3, x4, x5)
U54_ggggaa(x0, x1, x2, x3, x4, x5)
lecH_in_gg(x0, x1)
U47_ggggaa(x0, x1, x2, x3, x4, x5)
U49_ggggaa(x0, x1, x2, x3, x4, x5)
gtcI_in_gg(x0, x1)
U53_ggggaa(x0, x1, x2, x3, x4, x5)
U55_ggggaa(x0, x1, x2, x3, x4, x5)
U44_gg(x0, x1, x2)
U50_gg(x0, x1, x2)

We have to consider all (P,Q,R)-chains.

(40) Rewriting (EQUIVALENT transformation)

By rewriting [LPAR04] the rule MERGESORTE_IN_GAA(.(X1, .(X2, X3))) → U4_GAA(X1, X2, X3, splitcD_in_ggaaa(X1, .(X2, X3))) at position [3] we obtained the following new rules [LPAR04]:

MERGESORTE_IN_GAA(.(X1, .(X2, X3))) → U4_GAA(X1, X2, X3, U37_ggaaa(X1, .(X2, X3), splitcA_in_gaaa(.(X2, X3))))

(41) Obligation:

Q DP problem:
The TRS P consists of the following rules:

U4_GAA(X1, X2, X3, splitcD_out_ggaaa(X1, .(X2, X3), X7, X8)) → MERGESORTE_IN_GAA(X7)
U4_GAA(X1, X2, X3, splitcD_out_ggaaa(X1, .(X2, X3), X7, X8)) → U6_GAA(X1, X2, X3, X8, mergesortcE_in_gaa(X7))
U6_GAA(X1, X2, X3, X8, mergesortcE_out_gaa(X7, X9)) → MERGESORTE_IN_GAA(X8)
MERGESORTE_IN_GAA(.(X1, .(X2, X3))) → U4_GAA(X1, X2, X3, U37_ggaaa(X1, .(X2, X3), splitcA_in_gaaa(.(X2, X3))))

The TRS R consists of the following rules:

splitcD_in_ggaaa(X1, X2) → U37_ggaaa(X1, X2, splitcA_in_gaaa(X2))
mergesortcE_in_gaa([]) → mergesortcE_out_gaa([], [])
mergesortcE_in_gaa(.(X1, [])) → mergesortcE_out_gaa(.(X1, []), .(X1, []))
mergesortcE_in_gaa(.(X1, .(X2, X3))) → U38_gaa(X1, X2, X3, splitcD_in_ggaaa(X1, .(X2, X3)))
U37_ggaaa(X1, X2, splitcA_out_gaaa(X2, X4, X3)) → splitcD_out_ggaaa(X1, X2, .(X1, X3), X4)
U38_gaa(X1, X2, X3, splitcD_out_ggaaa(X1, .(X2, X3), X7, X8)) → U39_gaa(X1, X2, X3, X8, mergesortcE_in_gaa(X7))
splitcA_in_gaaa([]) → splitcA_out_gaaa([], [], [])
splitcA_in_gaaa(.(X1, X2)) → U32_gaaa(X1, X2, splitcA_in_gaaa(X2))
U39_gaa(X1, X2, X3, X8, mergesortcE_out_gaa(X7, X9)) → U40_gaa(X1, X2, X3, X9, mergesortcE_in_gaa(X8))
U32_gaaa(X1, X2, splitcA_out_gaaa(X2, X4, X3)) → splitcA_out_gaaa(.(X1, X2), .(X1, X3), X4)
U40_gaa(X1, X2, X3, X9, mergesortcE_out_gaa(X8, X10)) → U41_gaa(X1, X2, X3, mergecC_in_ggaaa(X9, X10))
U41_gaa(X1, X2, X3, mergecC_out_ggaaa(X9, X10, X4)) → mergesortcE_out_gaa(.(X1, .(X2, X3)), X4)
mergecC_in_ggaaa([], X1) → mergecC_out_ggaaa([], X1, X1)
mergecC_in_ggaaa(X1, []) → mergecC_out_ggaaa(X1, [], X1)
mergecC_in_ggaaa(.(X1, X2), .(X3, X4)) → U42_ggaaa(X1, X2, X3, X4, qcF_in_ggggaa(X1, X3, X2, X4))
mergecC_in_ggaaa(.(X1, X2), .(X3, X4)) → U43_ggaaa(X1, X2, X3, X4, qcG_in_ggggaa(X1, X3, X2, X4))
U42_ggaaa(X1, X2, X3, X4, qcF_out_ggggaa(X1, X3, X2, X4, X5)) → mergecC_out_ggaaa(.(X1, X2), .(X3, X4), .(X1, X5))
U43_ggaaa(X1, X2, X3, X4, qcG_out_ggggaa(X1, X3, X2, X4, X5)) → mergecC_out_ggaaa(.(X1, X2), .(X3, X4), .(X3, X5))
qcF_in_ggggaa(X1, X2, [], X3) → U45_ggggaa(X1, X2, X3, lecH_in_gg(X1, X2))
qcF_in_ggggaa(X1, X2, .(X3, X4), X5) → U46_ggggaa(X1, X2, X3, X4, X5, lecH_in_gg(X1, X2))
qcF_in_ggggaa(X1, X2, .(X3, X4), X5) → U48_ggggaa(X1, X2, X3, X4, X5, lecH_in_gg(X1, X2))
qcG_in_ggggaa(X1, X2, X3, []) → U51_ggggaa(X1, X2, X3, gtcI_in_gg(X1, X2))
qcG_in_ggggaa(X1, X2, X3, .(X4, X5)) → U52_ggggaa(X1, X2, X3, X4, X5, gtcI_in_gg(X1, X2))
qcG_in_ggggaa(X1, X2, X3, .(X4, X5)) → U54_ggggaa(X1, X2, X3, X4, X5, gtcI_in_gg(X1, X2))
U45_ggggaa(X1, X2, X3, lecH_out_gg(X1, X2)) → qcF_out_ggggaa(X1, X2, [], X3, .(X2, X3))
U46_ggggaa(X1, X2, X3, X4, X5, lecH_out_gg(X1, X2)) → U47_ggggaa(X1, X2, X3, X4, X5, qcF_in_ggggaa(X3, X2, X4, X5))
U48_ggggaa(X1, X2, X3, X4, X5, lecH_out_gg(X1, X2)) → U49_ggggaa(X1, X2, X3, X4, X5, qcG_in_ggggaa(X3, X2, X4, X5))
U51_ggggaa(X1, X2, X3, gtcI_out_gg(X1, X2)) → qcG_out_ggggaa(X1, X2, X3, [], .(X1, X3))
U52_ggggaa(X1, X2, X3, X4, X5, gtcI_out_gg(X1, X2)) → U53_ggggaa(X1, X2, X3, X4, X5, qcF_in_ggggaa(X1, X4, X3, X5))
U54_ggggaa(X1, X2, X3, X4, X5, gtcI_out_gg(X1, X2)) → U55_ggggaa(X1, X2, X3, X4, X5, qcG_in_ggggaa(X1, X4, X3, X5))
lecH_in_gg(s(X1), s(X2)) → U44_gg(X1, X2, lecH_in_gg(X1, X2))
lecH_in_gg(0, s(0)) → lecH_out_gg(0, s(0))
lecH_in_gg(0, 0) → lecH_out_gg(0, 0)
U47_ggggaa(X1, X2, X3, X4, X5, qcF_out_ggggaa(X3, X2, X4, X5, X6)) → qcF_out_ggggaa(X1, X2, .(X3, X4), X5, .(X3, X6))
U49_ggggaa(X1, X2, X3, X4, X5, qcG_out_ggggaa(X3, X2, X4, X5, X6)) → qcF_out_ggggaa(X1, X2, .(X3, X4), X5, .(X2, X6))
gtcI_in_gg(s(X1), s(X2)) → U50_gg(X1, X2, gtcI_in_gg(X1, X2))
gtcI_in_gg(s(0), 0) → gtcI_out_gg(s(0), 0)
U53_ggggaa(X1, X2, X3, X4, X5, qcF_out_ggggaa(X1, X4, X3, X5, X6)) → qcG_out_ggggaa(X1, X2, X3, .(X4, X5), .(X1, X6))
U55_ggggaa(X1, X2, X3, X4, X5, qcG_out_ggggaa(X1, X4, X3, X5, X6)) → qcG_out_ggggaa(X1, X2, X3, .(X4, X5), .(X4, X6))
U44_gg(X1, X2, lecH_out_gg(X1, X2)) → lecH_out_gg(s(X1), s(X2))
U50_gg(X1, X2, gtcI_out_gg(X1, X2)) → gtcI_out_gg(s(X1), s(X2))

The set Q consists of the following terms:

splitcD_in_ggaaa(x0, x1)
mergesortcE_in_gaa(x0)
U37_ggaaa(x0, x1, x2)
U38_gaa(x0, x1, x2, x3)
splitcA_in_gaaa(x0)
U39_gaa(x0, x1, x2, x3, x4)
U32_gaaa(x0, x1, x2)
U40_gaa(x0, x1, x2, x3, x4)
U41_gaa(x0, x1, x2, x3)
mergecC_in_ggaaa(x0, x1)
U42_ggaaa(x0, x1, x2, x3, x4)
U43_ggaaa(x0, x1, x2, x3, x4)
qcF_in_ggggaa(x0, x1, x2, x3)
qcG_in_ggggaa(x0, x1, x2, x3)
U45_ggggaa(x0, x1, x2, x3)
U46_ggggaa(x0, x1, x2, x3, x4, x5)
U48_ggggaa(x0, x1, x2, x3, x4, x5)
U51_ggggaa(x0, x1, x2, x3)
U52_ggggaa(x0, x1, x2, x3, x4, x5)
U54_ggggaa(x0, x1, x2, x3, x4, x5)
lecH_in_gg(x0, x1)
U47_ggggaa(x0, x1, x2, x3, x4, x5)
U49_ggggaa(x0, x1, x2, x3, x4, x5)
gtcI_in_gg(x0, x1)
U53_ggggaa(x0, x1, x2, x3, x4, x5)
U55_ggggaa(x0, x1, x2, x3, x4, x5)
U44_gg(x0, x1, x2)
U50_gg(x0, x1, x2)

We have to consider all (P,Q,R)-chains.

(42) Rewriting (EQUIVALENT transformation)

By rewriting [LPAR04] the rule MERGESORTE_IN_GAA(.(X1, .(X2, X3))) → U4_GAA(X1, X2, X3, U37_ggaaa(X1, .(X2, X3), splitcA_in_gaaa(.(X2, X3)))) at position [3,2] we obtained the following new rules [LPAR04]:

MERGESORTE_IN_GAA(.(X1, .(X2, X3))) → U4_GAA(X1, X2, X3, U37_ggaaa(X1, .(X2, X3), U32_gaaa(X2, X3, splitcA_in_gaaa(X3))))

(43) Obligation:

Q DP problem:
The TRS P consists of the following rules:

U4_GAA(X1, X2, X3, splitcD_out_ggaaa(X1, .(X2, X3), X7, X8)) → MERGESORTE_IN_GAA(X7)
U4_GAA(X1, X2, X3, splitcD_out_ggaaa(X1, .(X2, X3), X7, X8)) → U6_GAA(X1, X2, X3, X8, mergesortcE_in_gaa(X7))
U6_GAA(X1, X2, X3, X8, mergesortcE_out_gaa(X7, X9)) → MERGESORTE_IN_GAA(X8)
MERGESORTE_IN_GAA(.(X1, .(X2, X3))) → U4_GAA(X1, X2, X3, U37_ggaaa(X1, .(X2, X3), U32_gaaa(X2, X3, splitcA_in_gaaa(X3))))

The TRS R consists of the following rules:

splitcD_in_ggaaa(X1, X2) → U37_ggaaa(X1, X2, splitcA_in_gaaa(X2))
mergesortcE_in_gaa([]) → mergesortcE_out_gaa([], [])
mergesortcE_in_gaa(.(X1, [])) → mergesortcE_out_gaa(.(X1, []), .(X1, []))
mergesortcE_in_gaa(.(X1, .(X2, X3))) → U38_gaa(X1, X2, X3, splitcD_in_ggaaa(X1, .(X2, X3)))
U37_ggaaa(X1, X2, splitcA_out_gaaa(X2, X4, X3)) → splitcD_out_ggaaa(X1, X2, .(X1, X3), X4)
U38_gaa(X1, X2, X3, splitcD_out_ggaaa(X1, .(X2, X3), X7, X8)) → U39_gaa(X1, X2, X3, X8, mergesortcE_in_gaa(X7))
splitcA_in_gaaa([]) → splitcA_out_gaaa([], [], [])
splitcA_in_gaaa(.(X1, X2)) → U32_gaaa(X1, X2, splitcA_in_gaaa(X2))
U39_gaa(X1, X2, X3, X8, mergesortcE_out_gaa(X7, X9)) → U40_gaa(X1, X2, X3, X9, mergesortcE_in_gaa(X8))
U32_gaaa(X1, X2, splitcA_out_gaaa(X2, X4, X3)) → splitcA_out_gaaa(.(X1, X2), .(X1, X3), X4)
U40_gaa(X1, X2, X3, X9, mergesortcE_out_gaa(X8, X10)) → U41_gaa(X1, X2, X3, mergecC_in_ggaaa(X9, X10))
U41_gaa(X1, X2, X3, mergecC_out_ggaaa(X9, X10, X4)) → mergesortcE_out_gaa(.(X1, .(X2, X3)), X4)
mergecC_in_ggaaa([], X1) → mergecC_out_ggaaa([], X1, X1)
mergecC_in_ggaaa(X1, []) → mergecC_out_ggaaa(X1, [], X1)
mergecC_in_ggaaa(.(X1, X2), .(X3, X4)) → U42_ggaaa(X1, X2, X3, X4, qcF_in_ggggaa(X1, X3, X2, X4))
mergecC_in_ggaaa(.(X1, X2), .(X3, X4)) → U43_ggaaa(X1, X2, X3, X4, qcG_in_ggggaa(X1, X3, X2, X4))
U42_ggaaa(X1, X2, X3, X4, qcF_out_ggggaa(X1, X3, X2, X4, X5)) → mergecC_out_ggaaa(.(X1, X2), .(X3, X4), .(X1, X5))
U43_ggaaa(X1, X2, X3, X4, qcG_out_ggggaa(X1, X3, X2, X4, X5)) → mergecC_out_ggaaa(.(X1, X2), .(X3, X4), .(X3, X5))
qcF_in_ggggaa(X1, X2, [], X3) → U45_ggggaa(X1, X2, X3, lecH_in_gg(X1, X2))
qcF_in_ggggaa(X1, X2, .(X3, X4), X5) → U46_ggggaa(X1, X2, X3, X4, X5, lecH_in_gg(X1, X2))
qcF_in_ggggaa(X1, X2, .(X3, X4), X5) → U48_ggggaa(X1, X2, X3, X4, X5, lecH_in_gg(X1, X2))
qcG_in_ggggaa(X1, X2, X3, []) → U51_ggggaa(X1, X2, X3, gtcI_in_gg(X1, X2))
qcG_in_ggggaa(X1, X2, X3, .(X4, X5)) → U52_ggggaa(X1, X2, X3, X4, X5, gtcI_in_gg(X1, X2))
qcG_in_ggggaa(X1, X2, X3, .(X4, X5)) → U54_ggggaa(X1, X2, X3, X4, X5, gtcI_in_gg(X1, X2))
U45_ggggaa(X1, X2, X3, lecH_out_gg(X1, X2)) → qcF_out_ggggaa(X1, X2, [], X3, .(X2, X3))
U46_ggggaa(X1, X2, X3, X4, X5, lecH_out_gg(X1, X2)) → U47_ggggaa(X1, X2, X3, X4, X5, qcF_in_ggggaa(X3, X2, X4, X5))
U48_ggggaa(X1, X2, X3, X4, X5, lecH_out_gg(X1, X2)) → U49_ggggaa(X1, X2, X3, X4, X5, qcG_in_ggggaa(X3, X2, X4, X5))
U51_ggggaa(X1, X2, X3, gtcI_out_gg(X1, X2)) → qcG_out_ggggaa(X1, X2, X3, [], .(X1, X3))
U52_ggggaa(X1, X2, X3, X4, X5, gtcI_out_gg(X1, X2)) → U53_ggggaa(X1, X2, X3, X4, X5, qcF_in_ggggaa(X1, X4, X3, X5))
U54_ggggaa(X1, X2, X3, X4, X5, gtcI_out_gg(X1, X2)) → U55_ggggaa(X1, X2, X3, X4, X5, qcG_in_ggggaa(X1, X4, X3, X5))
lecH_in_gg(s(X1), s(X2)) → U44_gg(X1, X2, lecH_in_gg(X1, X2))
lecH_in_gg(0, s(0)) → lecH_out_gg(0, s(0))
lecH_in_gg(0, 0) → lecH_out_gg(0, 0)
U47_ggggaa(X1, X2, X3, X4, X5, qcF_out_ggggaa(X3, X2, X4, X5, X6)) → qcF_out_ggggaa(X1, X2, .(X3, X4), X5, .(X3, X6))
U49_ggggaa(X1, X2, X3, X4, X5, qcG_out_ggggaa(X3, X2, X4, X5, X6)) → qcF_out_ggggaa(X1, X2, .(X3, X4), X5, .(X2, X6))
gtcI_in_gg(s(X1), s(X2)) → U50_gg(X1, X2, gtcI_in_gg(X1, X2))
gtcI_in_gg(s(0), 0) → gtcI_out_gg(s(0), 0)
U53_ggggaa(X1, X2, X3, X4, X5, qcF_out_ggggaa(X1, X4, X3, X5, X6)) → qcG_out_ggggaa(X1, X2, X3, .(X4, X5), .(X1, X6))
U55_ggggaa(X1, X2, X3, X4, X5, qcG_out_ggggaa(X1, X4, X3, X5, X6)) → qcG_out_ggggaa(X1, X2, X3, .(X4, X5), .(X4, X6))
U44_gg(X1, X2, lecH_out_gg(X1, X2)) → lecH_out_gg(s(X1), s(X2))
U50_gg(X1, X2, gtcI_out_gg(X1, X2)) → gtcI_out_gg(s(X1), s(X2))

The set Q consists of the following terms:

splitcD_in_ggaaa(x0, x1)
mergesortcE_in_gaa(x0)
U37_ggaaa(x0, x1, x2)
U38_gaa(x0, x1, x2, x3)
splitcA_in_gaaa(x0)
U39_gaa(x0, x1, x2, x3, x4)
U32_gaaa(x0, x1, x2)
U40_gaa(x0, x1, x2, x3, x4)
U41_gaa(x0, x1, x2, x3)
mergecC_in_ggaaa(x0, x1)
U42_ggaaa(x0, x1, x2, x3, x4)
U43_ggaaa(x0, x1, x2, x3, x4)
qcF_in_ggggaa(x0, x1, x2, x3)
qcG_in_ggggaa(x0, x1, x2, x3)
U45_ggggaa(x0, x1, x2, x3)
U46_ggggaa(x0, x1, x2, x3, x4, x5)
U48_ggggaa(x0, x1, x2, x3, x4, x5)
U51_ggggaa(x0, x1, x2, x3)
U52_ggggaa(x0, x1, x2, x3, x4, x5)
U54_ggggaa(x0, x1, x2, x3, x4, x5)
lecH_in_gg(x0, x1)
U47_ggggaa(x0, x1, x2, x3, x4, x5)
U49_ggggaa(x0, x1, x2, x3, x4, x5)
gtcI_in_gg(x0, x1)
U53_ggggaa(x0, x1, x2, x3, x4, x5)
U55_ggggaa(x0, x1, x2, x3, x4, x5)
U44_gg(x0, x1, x2)
U50_gg(x0, x1, x2)

We have to consider all (P,Q,R)-chains.

(44) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04,JAR06].


The following pairs can be oriented strictly and are deleted.


U4_GAA(X1, X2, X3, splitcD_out_ggaaa(X1, .(X2, X3), X7, X8)) → MERGESORTE_IN_GAA(X7)
U4_GAA(X1, X2, X3, splitcD_out_ggaaa(X1, .(X2, X3), X7, X8)) → U6_GAA(X1, X2, X3, X8, mergesortcE_in_gaa(X7))
MERGESORTE_IN_GAA(.(X1, .(X2, X3))) → U4_GAA(X1, X2, X3, U37_ggaaa(X1, .(X2, X3), U32_gaaa(X2, X3, splitcA_in_gaaa(X3))))
The remaining pairs can at least be oriented weakly.
Used ordering: Polynomial Order [NEGPOLO,POLO] with Interpretation:

POL( U6_GAA(x1, ..., x5) ) = 2x4 + 2x5 + 1


POL( mergesortcE_in_gaa(x1) ) = x1


POL( [] ) = 0


POL( mergesortcE_out_gaa(x1, x2) ) = max{0, -2}


POL( .(x1, x2) ) = 2x2 + 2


POL( U38_gaa(x1, ..., x4) ) = 2x3 + 2


POL( splitcD_in_ggaaa(x1, x2) ) = max{0, 2x1 - 2}


POL( U32_gaaa(x1, ..., x3) ) = 2x3 + 2


POL( U37_ggaaa(x1, ..., x3) ) = x3 + 2


POL( U4_GAA(x1, ..., x4) ) = 2x4 + 2


POL( splitcA_in_gaaa(x1) ) = x1


POL( splitcA_out_gaaa(x1, ..., x3) ) = x2 + 2x3


POL( splitcD_out_ggaaa(x1, ..., x4) ) = x3 + x4


POL( U39_gaa(x1, ..., x5) ) = x3 + 1


POL( U40_gaa(x1, ..., x5) ) = 1


POL( U41_gaa(x1, ..., x4) ) = max{0, -1}


POL( mergecC_in_ggaaa(x1, x2) ) = 1


POL( mergecC_out_ggaaa(x1, ..., x3) ) = x1 + 2x2


POL( U42_ggaaa(x1, ..., x5) ) = max{0, x3 + x4 + x5 - 2}


POL( qcF_in_ggggaa(x1, ..., x4) ) = x2 + x3 + 1


POL( U43_ggaaa(x1, ..., x5) ) = max{0, 2x1 + 2x3 + x4 - 2}


POL( qcG_in_ggggaa(x1, ..., x4) ) = 2x1 + 2x2 + 1


POL( U47_ggggaa(x1, ..., x6) ) = x2 + x3 + 1


POL( U53_ggggaa(x1, ..., x6) ) = max{0, 2x2 + x4 + 2x5 - 2}


POL( U45_ggggaa(x1, ..., x4) ) = x1 + 2x2 + 2


POL( lecH_in_gg(x1, x2) ) = 2


POL( U46_ggggaa(x1, ..., x6) ) = x1 + x4 + 2x5 + x6 + 2


POL( U48_ggggaa(x1, ..., x6) ) = max{0, x1 + x3 + x4 - 2}


POL( qcF_out_ggggaa(x1, ..., x5) ) = max{0, x1 + x4 - 1}


POL( U49_ggggaa(x1, ..., x6) ) = max{0, 2x2 + x5 - 1}


POL( U55_ggggaa(x1, ..., x6) ) = x1 + 2x2 + x3 + 2x4 + 2x5 + 2x6 + 2


POL( U51_ggggaa(x1, ..., x4) ) = x1 + 2x2 + x3 + 2


POL( gtcI_in_gg(x1, x2) ) = 2


POL( U52_ggggaa(x1, ..., x6) ) = max{0, 2x1 + x2 + x3 + 2x4 + 2x5 + 2x6 - 2}


POL( U54_ggggaa(x1, ..., x6) ) = max{0, x6 - 1}


POL( qcG_out_ggggaa(x1, ..., x5) ) = x2 + 2x5 + 2


POL( s(x1) ) = max{0, 2x1 - 2}


POL( U44_gg(x1, ..., x3) ) = x1 + x2 + 2x3 + 2


POL( 0 ) = 0


POL( lecH_out_gg(x1, x2) ) = max{0, x1 - 1}


POL( U50_gg(x1, ..., x3) ) = x1 + 2


POL( gtcI_out_gg(x1, x2) ) = 0


POL( MERGESORTE_IN_GAA(x1) ) = 2x1 + 1



The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented:

mergesortcE_in_gaa([]) → mergesortcE_out_gaa([], [])
mergesortcE_in_gaa(.(X1, [])) → mergesortcE_out_gaa(.(X1, []), .(X1, []))
mergesortcE_in_gaa(.(X1, .(X2, X3))) → U38_gaa(X1, X2, X3, splitcD_in_ggaaa(X1, .(X2, X3)))
splitcA_in_gaaa([]) → splitcA_out_gaaa([], [], [])
splitcA_in_gaaa(.(X1, X2)) → U32_gaaa(X1, X2, splitcA_in_gaaa(X2))
U32_gaaa(X1, X2, splitcA_out_gaaa(X2, X4, X3)) → splitcA_out_gaaa(.(X1, X2), .(X1, X3), X4)
U37_ggaaa(X1, X2, splitcA_out_gaaa(X2, X4, X3)) → splitcD_out_ggaaa(X1, X2, .(X1, X3), X4)
U38_gaa(X1, X2, X3, splitcD_out_ggaaa(X1, .(X2, X3), X7, X8)) → U39_gaa(X1, X2, X3, X8, mergesortcE_in_gaa(X7))
U39_gaa(X1, X2, X3, X8, mergesortcE_out_gaa(X7, X9)) → U40_gaa(X1, X2, X3, X9, mergesortcE_in_gaa(X8))
U40_gaa(X1, X2, X3, X9, mergesortcE_out_gaa(X8, X10)) → U41_gaa(X1, X2, X3, mergecC_in_ggaaa(X9, X10))
U41_gaa(X1, X2, X3, mergecC_out_ggaaa(X9, X10, X4)) → mergesortcE_out_gaa(.(X1, .(X2, X3)), X4)

(45) Obligation:

Q DP problem:
The TRS P consists of the following rules:

U6_GAA(X1, X2, X3, X8, mergesortcE_out_gaa(X7, X9)) → MERGESORTE_IN_GAA(X8)

The TRS R consists of the following rules:

splitcD_in_ggaaa(X1, X2) → U37_ggaaa(X1, X2, splitcA_in_gaaa(X2))
mergesortcE_in_gaa([]) → mergesortcE_out_gaa([], [])
mergesortcE_in_gaa(.(X1, [])) → mergesortcE_out_gaa(.(X1, []), .(X1, []))
mergesortcE_in_gaa(.(X1, .(X2, X3))) → U38_gaa(X1, X2, X3, splitcD_in_ggaaa(X1, .(X2, X3)))
U37_ggaaa(X1, X2, splitcA_out_gaaa(X2, X4, X3)) → splitcD_out_ggaaa(X1, X2, .(X1, X3), X4)
U38_gaa(X1, X2, X3, splitcD_out_ggaaa(X1, .(X2, X3), X7, X8)) → U39_gaa(X1, X2, X3, X8, mergesortcE_in_gaa(X7))
splitcA_in_gaaa([]) → splitcA_out_gaaa([], [], [])
splitcA_in_gaaa(.(X1, X2)) → U32_gaaa(X1, X2, splitcA_in_gaaa(X2))
U39_gaa(X1, X2, X3, X8, mergesortcE_out_gaa(X7, X9)) → U40_gaa(X1, X2, X3, X9, mergesortcE_in_gaa(X8))
U32_gaaa(X1, X2, splitcA_out_gaaa(X2, X4, X3)) → splitcA_out_gaaa(.(X1, X2), .(X1, X3), X4)
U40_gaa(X1, X2, X3, X9, mergesortcE_out_gaa(X8, X10)) → U41_gaa(X1, X2, X3, mergecC_in_ggaaa(X9, X10))
U41_gaa(X1, X2, X3, mergecC_out_ggaaa(X9, X10, X4)) → mergesortcE_out_gaa(.(X1, .(X2, X3)), X4)
mergecC_in_ggaaa([], X1) → mergecC_out_ggaaa([], X1, X1)
mergecC_in_ggaaa(X1, []) → mergecC_out_ggaaa(X1, [], X1)
mergecC_in_ggaaa(.(X1, X2), .(X3, X4)) → U42_ggaaa(X1, X2, X3, X4, qcF_in_ggggaa(X1, X3, X2, X4))
mergecC_in_ggaaa(.(X1, X2), .(X3, X4)) → U43_ggaaa(X1, X2, X3, X4, qcG_in_ggggaa(X1, X3, X2, X4))
U42_ggaaa(X1, X2, X3, X4, qcF_out_ggggaa(X1, X3, X2, X4, X5)) → mergecC_out_ggaaa(.(X1, X2), .(X3, X4), .(X1, X5))
U43_ggaaa(X1, X2, X3, X4, qcG_out_ggggaa(X1, X3, X2, X4, X5)) → mergecC_out_ggaaa(.(X1, X2), .(X3, X4), .(X3, X5))
qcF_in_ggggaa(X1, X2, [], X3) → U45_ggggaa(X1, X2, X3, lecH_in_gg(X1, X2))
qcF_in_ggggaa(X1, X2, .(X3, X4), X5) → U46_ggggaa(X1, X2, X3, X4, X5, lecH_in_gg(X1, X2))
qcF_in_ggggaa(X1, X2, .(X3, X4), X5) → U48_ggggaa(X1, X2, X3, X4, X5, lecH_in_gg(X1, X2))
qcG_in_ggggaa(X1, X2, X3, []) → U51_ggggaa(X1, X2, X3, gtcI_in_gg(X1, X2))
qcG_in_ggggaa(X1, X2, X3, .(X4, X5)) → U52_ggggaa(X1, X2, X3, X4, X5, gtcI_in_gg(X1, X2))
qcG_in_ggggaa(X1, X2, X3, .(X4, X5)) → U54_ggggaa(X1, X2, X3, X4, X5, gtcI_in_gg(X1, X2))
U45_ggggaa(X1, X2, X3, lecH_out_gg(X1, X2)) → qcF_out_ggggaa(X1, X2, [], X3, .(X2, X3))
U46_ggggaa(X1, X2, X3, X4, X5, lecH_out_gg(X1, X2)) → U47_ggggaa(X1, X2, X3, X4, X5, qcF_in_ggggaa(X3, X2, X4, X5))
U48_ggggaa(X1, X2, X3, X4, X5, lecH_out_gg(X1, X2)) → U49_ggggaa(X1, X2, X3, X4, X5, qcG_in_ggggaa(X3, X2, X4, X5))
U51_ggggaa(X1, X2, X3, gtcI_out_gg(X1, X2)) → qcG_out_ggggaa(X1, X2, X3, [], .(X1, X3))
U52_ggggaa(X1, X2, X3, X4, X5, gtcI_out_gg(X1, X2)) → U53_ggggaa(X1, X2, X3, X4, X5, qcF_in_ggggaa(X1, X4, X3, X5))
U54_ggggaa(X1, X2, X3, X4, X5, gtcI_out_gg(X1, X2)) → U55_ggggaa(X1, X2, X3, X4, X5, qcG_in_ggggaa(X1, X4, X3, X5))
lecH_in_gg(s(X1), s(X2)) → U44_gg(X1, X2, lecH_in_gg(X1, X2))
lecH_in_gg(0, s(0)) → lecH_out_gg(0, s(0))
lecH_in_gg(0, 0) → lecH_out_gg(0, 0)
U47_ggggaa(X1, X2, X3, X4, X5, qcF_out_ggggaa(X3, X2, X4, X5, X6)) → qcF_out_ggggaa(X1, X2, .(X3, X4), X5, .(X3, X6))
U49_ggggaa(X1, X2, X3, X4, X5, qcG_out_ggggaa(X3, X2, X4, X5, X6)) → qcF_out_ggggaa(X1, X2, .(X3, X4), X5, .(X2, X6))
gtcI_in_gg(s(X1), s(X2)) → U50_gg(X1, X2, gtcI_in_gg(X1, X2))
gtcI_in_gg(s(0), 0) → gtcI_out_gg(s(0), 0)
U53_ggggaa(X1, X2, X3, X4, X5, qcF_out_ggggaa(X1, X4, X3, X5, X6)) → qcG_out_ggggaa(X1, X2, X3, .(X4, X5), .(X1, X6))
U55_ggggaa(X1, X2, X3, X4, X5, qcG_out_ggggaa(X1, X4, X3, X5, X6)) → qcG_out_ggggaa(X1, X2, X3, .(X4, X5), .(X4, X6))
U44_gg(X1, X2, lecH_out_gg(X1, X2)) → lecH_out_gg(s(X1), s(X2))
U50_gg(X1, X2, gtcI_out_gg(X1, X2)) → gtcI_out_gg(s(X1), s(X2))

The set Q consists of the following terms:

splitcD_in_ggaaa(x0, x1)
mergesortcE_in_gaa(x0)
U37_ggaaa(x0, x1, x2)
U38_gaa(x0, x1, x2, x3)
splitcA_in_gaaa(x0)
U39_gaa(x0, x1, x2, x3, x4)
U32_gaaa(x0, x1, x2)
U40_gaa(x0, x1, x2, x3, x4)
U41_gaa(x0, x1, x2, x3)
mergecC_in_ggaaa(x0, x1)
U42_ggaaa(x0, x1, x2, x3, x4)
U43_ggaaa(x0, x1, x2, x3, x4)
qcF_in_ggggaa(x0, x1, x2, x3)
qcG_in_ggggaa(x0, x1, x2, x3)
U45_ggggaa(x0, x1, x2, x3)
U46_ggggaa(x0, x1, x2, x3, x4, x5)
U48_ggggaa(x0, x1, x2, x3, x4, x5)
U51_ggggaa(x0, x1, x2, x3)
U52_ggggaa(x0, x1, x2, x3, x4, x5)
U54_ggggaa(x0, x1, x2, x3, x4, x5)
lecH_in_gg(x0, x1)
U47_ggggaa(x0, x1, x2, x3, x4, x5)
U49_ggggaa(x0, x1, x2, x3, x4, x5)
gtcI_in_gg(x0, x1)
U53_ggggaa(x0, x1, x2, x3, x4, x5)
U55_ggggaa(x0, x1, x2, x3, x4, x5)
U44_gg(x0, x1, x2)
U50_gg(x0, x1, x2)

We have to consider all (P,Q,R)-chains.

(46) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs with 1 less node.

(47) TRUE

(48) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

MERGESORTB_IN_GAA(.(X1, .(X2, X3)), X4, .(X5, X6)) → U25_GAA(X1, X2, X3, X4, X5, X6, splitcD_in_ggaaa(X2, X3, X7, X8, X6))
U25_GAA(X1, X2, X3, X4, X5, X6, splitcD_out_ggaaa(X2, X3, X7, X8, X6)) → MERGESORTB_IN_GAA(.(X1, X8), X9, X6)

The TRS R consists of the following rules:

splitcD_in_ggaaa(X1, X2, .(X1, X3), X4, .(X5, X6)) → U37_ggaaa(X1, X2, X3, X4, X5, X6, splitcA_in_gaaa(X2, X4, X3, X6))
splitcA_in_gaaa([], [], [], X1) → splitcA_out_gaaa([], [], [], X1)
splitcA_in_gaaa(.(X1, X2), .(X1, X3), X4, .(X5, X6)) → U32_gaaa(X1, X2, X3, X4, X5, X6, splitcA_in_gaaa(X2, X4, X3, X6))
U32_gaaa(X1, X2, X3, X4, X5, X6, splitcA_out_gaaa(X2, X4, X3, X6)) → splitcA_out_gaaa(.(X1, X2), .(X1, X3), X4, .(X5, X6))
U37_ggaaa(X1, X2, X3, X4, X5, X6, splitcA_out_gaaa(X2, X4, X3, X6)) → splitcD_out_ggaaa(X1, X2, .(X1, X3), X4, .(X5, X6))
mergesortcB_in_gaa([], [], X1) → mergesortcB_out_gaa([], [], X1)
mergesortcB_in_gaa(.(X1, []), .(X1, []), X2) → mergesortcB_out_gaa(.(X1, []), .(X1, []), X2)
mergesortcB_in_gaa(.(X1, .(X2, X3)), X4, .(X5, X6)) → U33_gaa(X1, X2, X3, X4, X5, X6, splitcD_in_ggaaa(X2, X3, X7, X8, X6))
U33_gaa(X1, X2, X3, X4, X5, X6, splitcD_out_ggaaa(X2, X3, X7, X8, X6)) → U34_gaa(X1, X2, X3, X4, X5, X6, X7, mergesortcB_in_gaa(.(X1, X8), X9, X6))
U34_gaa(X1, X2, X3, X4, X5, X6, X7, mergesortcB_out_gaa(.(X1, X8), X9, X6)) → U35_gaa(X1, X2, X3, X4, X5, X6, X9, mergesortcE_in_gaa(X7, X10, X6))
mergesortcE_in_gaa([], [], X1) → mergesortcE_out_gaa([], [], X1)
mergesortcE_in_gaa(.(X1, []), .(X1, []), X2) → mergesortcE_out_gaa(.(X1, []), .(X1, []), X2)
mergesortcE_in_gaa(.(X1, .(X2, X3)), X4, .(X5, X6)) → U38_gaa(X1, X2, X3, X4, X5, X6, splitcD_in_ggaaa(X1, .(X2, X3), X7, X8, .(X5, X6)))
U38_gaa(X1, X2, X3, X4, X5, X6, splitcD_out_ggaaa(X1, .(X2, X3), X7, X8, .(X5, X6))) → U39_gaa(X1, X2, X3, X4, X5, X6, X8, mergesortcE_in_gaa(X7, X9, X6))
U39_gaa(X1, X2, X3, X4, X5, X6, X8, mergesortcE_out_gaa(X7, X9, X6)) → U40_gaa(X1, X2, X3, X4, X5, X6, X9, mergesortcE_in_gaa(X8, X10, X6))
U40_gaa(X1, X2, X3, X4, X5, X6, X9, mergesortcE_out_gaa(X8, X10, X6)) → U41_gaa(X1, X2, X3, X4, X5, X6, mergecC_in_ggaaa(X9, X10, X4, X5, X6))
mergecC_in_ggaaa([], X1, X1, X2, X3) → mergecC_out_ggaaa([], X1, X1, X2, X3)
mergecC_in_ggaaa(X1, [], X1, X2, X3) → mergecC_out_ggaaa(X1, [], X1, X2, X3)
mergecC_in_ggaaa(.(X1, X2), .(X3, X4), .(X1, X5), X6, X7) → U42_ggaaa(X1, X2, X3, X4, X5, X6, X7, qcF_in_ggggaa(X1, X3, X2, X4, X5, X7))
qcF_in_ggggaa(X1, X2, [], X3, .(X2, X3), X4) → U45_ggggaa(X1, X2, X3, X4, lecH_in_gg(X1, X2))
lecH_in_gg(s(X1), s(X2)) → U44_gg(X1, X2, lecH_in_gg(X1, X2))
lecH_in_gg(0, s(0)) → lecH_out_gg(0, s(0))
lecH_in_gg(0, 0) → lecH_out_gg(0, 0)
U44_gg(X1, X2, lecH_out_gg(X1, X2)) → lecH_out_gg(s(X1), s(X2))
U45_ggggaa(X1, X2, X3, X4, lecH_out_gg(X1, X2)) → qcF_out_ggggaa(X1, X2, [], X3, .(X2, X3), X4)
qcF_in_ggggaa(X1, X2, .(X3, X4), X5, .(X3, X6), .(X7, X8)) → U46_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, lecH_in_gg(X1, X2))
U46_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, lecH_out_gg(X1, X2)) → U47_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, qcF_in_ggggaa(X3, X2, X4, X5, X6, X8))
qcF_in_ggggaa(X1, X2, .(X3, X4), X5, .(X2, X6), .(X7, X8)) → U48_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, lecH_in_gg(X1, X2))
U48_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, lecH_out_gg(X1, X2)) → U49_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, qcG_in_ggggaa(X3, X2, X4, X5, X6, X8))
qcG_in_ggggaa(X1, X2, X3, [], .(X1, X3), X4) → U51_ggggaa(X1, X2, X3, X4, gtcI_in_gg(X1, X2))
gtcI_in_gg(s(X1), s(X2)) → U50_gg(X1, X2, gtcI_in_gg(X1, X2))
gtcI_in_gg(s(0), 0) → gtcI_out_gg(s(0), 0)
U50_gg(X1, X2, gtcI_out_gg(X1, X2)) → gtcI_out_gg(s(X1), s(X2))
U51_ggggaa(X1, X2, X3, X4, gtcI_out_gg(X1, X2)) → qcG_out_ggggaa(X1, X2, X3, [], .(X1, X3), X4)
qcG_in_ggggaa(X1, X2, X3, .(X4, X5), .(X1, X6), .(X7, X8)) → U52_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, gtcI_in_gg(X1, X2))
U52_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, gtcI_out_gg(X1, X2)) → U53_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, qcF_in_ggggaa(X1, X4, X3, X5, X6, X8))
U53_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, qcF_out_ggggaa(X1, X4, X3, X5, X6, X8)) → qcG_out_ggggaa(X1, X2, X3, .(X4, X5), .(X1, X6), .(X7, X8))
qcG_in_ggggaa(X1, X2, X3, .(X4, X5), .(X4, X6), .(X7, X8)) → U54_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, gtcI_in_gg(X1, X2))
U54_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, gtcI_out_gg(X1, X2)) → U55_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, qcG_in_ggggaa(X1, X4, X3, X5, X6, X8))
U55_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, qcG_out_ggggaa(X1, X4, X3, X5, X6, X8)) → qcG_out_ggggaa(X1, X2, X3, .(X4, X5), .(X4, X6), .(X7, X8))
U49_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, qcG_out_ggggaa(X3, X2, X4, X5, X6, X8)) → qcF_out_ggggaa(X1, X2, .(X3, X4), X5, .(X2, X6), .(X7, X8))
U47_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, qcF_out_ggggaa(X3, X2, X4, X5, X6, X8)) → qcF_out_ggggaa(X1, X2, .(X3, X4), X5, .(X3, X6), .(X7, X8))
U42_ggaaa(X1, X2, X3, X4, X5, X6, X7, qcF_out_ggggaa(X1, X3, X2, X4, X5, X7)) → mergecC_out_ggaaa(.(X1, X2), .(X3, X4), .(X1, X5), X6, X7)
mergecC_in_ggaaa(.(X1, X2), .(X3, X4), .(X3, X5), X6, X7) → U43_ggaaa(X1, X2, X3, X4, X5, X6, X7, qcG_in_ggggaa(X1, X3, X2, X4, X5, X7))
U43_ggaaa(X1, X2, X3, X4, X5, X6, X7, qcG_out_ggggaa(X1, X3, X2, X4, X5, X7)) → mergecC_out_ggaaa(.(X1, X2), .(X3, X4), .(X3, X5), X6, X7)
U41_gaa(X1, X2, X3, X4, X5, X6, mergecC_out_ggaaa(X9, X10, X4, X5, X6)) → mergesortcE_out_gaa(.(X1, .(X2, X3)), X4, .(X5, X6))
U35_gaa(X1, X2, X3, X4, X5, X6, X9, mergesortcE_out_gaa(X7, X10, X6)) → U36_gaa(X1, X2, X3, X4, X5, X6, mergecC_in_ggaaa(X9, X10, X4, X5, X6))
U36_gaa(X1, X2, X3, X4, X5, X6, mergecC_out_ggaaa(X9, X10, X4, X5, X6)) → mergesortcB_out_gaa(.(X1, .(X2, X3)), X4, .(X5, X6))

The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x1, x2)
splitcD_in_ggaaa(x1, x2, x3, x4, x5)  =  splitcD_in_ggaaa(x1, x2)
U37_ggaaa(x1, x2, x3, x4, x5, x6, x7)  =  U37_ggaaa(x1, x2, x7)
splitcA_in_gaaa(x1, x2, x3, x4)  =  splitcA_in_gaaa(x1)
[]  =  []
splitcA_out_gaaa(x1, x2, x3, x4)  =  splitcA_out_gaaa(x1, x2, x3)
U32_gaaa(x1, x2, x3, x4, x5, x6, x7)  =  U32_gaaa(x1, x2, x7)
splitcD_out_ggaaa(x1, x2, x3, x4, x5)  =  splitcD_out_ggaaa(x1, x2, x3, x4)
mergesortcB_in_gaa(x1, x2, x3)  =  mergesortcB_in_gaa(x1)
mergesortcB_out_gaa(x1, x2, x3)  =  mergesortcB_out_gaa(x1, x2)
U33_gaa(x1, x2, x3, x4, x5, x6, x7)  =  U33_gaa(x1, x2, x3, x7)
U34_gaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  U34_gaa(x1, x2, x3, x7, x8)
U35_gaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  U35_gaa(x1, x2, x3, x7, x8)
mergesortcE_in_gaa(x1, x2, x3)  =  mergesortcE_in_gaa(x1)
mergesortcE_out_gaa(x1, x2, x3)  =  mergesortcE_out_gaa(x1, x2)
U38_gaa(x1, x2, x3, x4, x5, x6, x7)  =  U38_gaa(x1, x2, x3, x7)
U39_gaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  U39_gaa(x1, x2, x3, x7, x8)
U40_gaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  U40_gaa(x1, x2, x3, x7, x8)
U41_gaa(x1, x2, x3, x4, x5, x6, x7)  =  U41_gaa(x1, x2, x3, x7)
mergecC_in_ggaaa(x1, x2, x3, x4, x5)  =  mergecC_in_ggaaa(x1, x2)
mergecC_out_ggaaa(x1, x2, x3, x4, x5)  =  mergecC_out_ggaaa(x1, x2, x3)
U42_ggaaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  U42_ggaaa(x1, x2, x3, x4, x8)
qcF_in_ggggaa(x1, x2, x3, x4, x5, x6)  =  qcF_in_ggggaa(x1, x2, x3, x4)
U45_ggggaa(x1, x2, x3, x4, x5)  =  U45_ggggaa(x1, x2, x3, x5)
lecH_in_gg(x1, x2)  =  lecH_in_gg(x1, x2)
s(x1)  =  s(x1)
U44_gg(x1, x2, x3)  =  U44_gg(x1, x2, x3)
0  =  0
lecH_out_gg(x1, x2)  =  lecH_out_gg(x1, x2)
qcF_out_ggggaa(x1, x2, x3, x4, x5, x6)  =  qcF_out_ggggaa(x1, x2, x3, x4, x5)
U46_ggggaa(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U46_ggggaa(x1, x2, x3, x4, x5, x9)
U47_ggggaa(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U47_ggggaa(x1, x2, x3, x4, x5, x9)
U48_ggggaa(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U48_ggggaa(x1, x2, x3, x4, x5, x9)
U49_ggggaa(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U49_ggggaa(x1, x2, x3, x4, x5, x9)
qcG_in_ggggaa(x1, x2, x3, x4, x5, x6)  =  qcG_in_ggggaa(x1, x2, x3, x4)
U51_ggggaa(x1, x2, x3, x4, x5)  =  U51_ggggaa(x1, x2, x3, x5)
gtcI_in_gg(x1, x2)  =  gtcI_in_gg(x1, x2)
U50_gg(x1, x2, x3)  =  U50_gg(x1, x2, x3)
gtcI_out_gg(x1, x2)  =  gtcI_out_gg(x1, x2)
qcG_out_ggggaa(x1, x2, x3, x4, x5, x6)  =  qcG_out_ggggaa(x1, x2, x3, x4, x5)
U52_ggggaa(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U52_ggggaa(x1, x2, x3, x4, x5, x9)
U53_ggggaa(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U53_ggggaa(x1, x2, x3, x4, x5, x9)
U54_ggggaa(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U54_ggggaa(x1, x2, x3, x4, x5, x9)
U55_ggggaa(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U55_ggggaa(x1, x2, x3, x4, x5, x9)
U43_ggaaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  U43_ggaaa(x1, x2, x3, x4, x8)
U36_gaa(x1, x2, x3, x4, x5, x6, x7)  =  U36_gaa(x1, x2, x3, x7)
MERGESORTB_IN_GAA(x1, x2, x3)  =  MERGESORTB_IN_GAA(x1)
U25_GAA(x1, x2, x3, x4, x5, x6, x7)  =  U25_GAA(x1, x2, x3, x7)

We have to consider all (P,R,Pi)-chains

(49) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(50) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

MERGESORTB_IN_GAA(.(X1, .(X2, X3)), X4, .(X5, X6)) → U25_GAA(X1, X2, X3, X4, X5, X6, splitcD_in_ggaaa(X2, X3, X7, X8, X6))
U25_GAA(X1, X2, X3, X4, X5, X6, splitcD_out_ggaaa(X2, X3, X7, X8, X6)) → MERGESORTB_IN_GAA(.(X1, X8), X9, X6)

The TRS R consists of the following rules:

splitcD_in_ggaaa(X1, X2, .(X1, X3), X4, .(X5, X6)) → U37_ggaaa(X1, X2, X3, X4, X5, X6, splitcA_in_gaaa(X2, X4, X3, X6))
U37_ggaaa(X1, X2, X3, X4, X5, X6, splitcA_out_gaaa(X2, X4, X3, X6)) → splitcD_out_ggaaa(X1, X2, .(X1, X3), X4, .(X5, X6))
splitcA_in_gaaa([], [], [], X1) → splitcA_out_gaaa([], [], [], X1)
splitcA_in_gaaa(.(X1, X2), .(X1, X3), X4, .(X5, X6)) → U32_gaaa(X1, X2, X3, X4, X5, X6, splitcA_in_gaaa(X2, X4, X3, X6))
U32_gaaa(X1, X2, X3, X4, X5, X6, splitcA_out_gaaa(X2, X4, X3, X6)) → splitcA_out_gaaa(.(X1, X2), .(X1, X3), X4, .(X5, X6))

The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x1, x2)
splitcD_in_ggaaa(x1, x2, x3, x4, x5)  =  splitcD_in_ggaaa(x1, x2)
U37_ggaaa(x1, x2, x3, x4, x5, x6, x7)  =  U37_ggaaa(x1, x2, x7)
splitcA_in_gaaa(x1, x2, x3, x4)  =  splitcA_in_gaaa(x1)
[]  =  []
splitcA_out_gaaa(x1, x2, x3, x4)  =  splitcA_out_gaaa(x1, x2, x3)
U32_gaaa(x1, x2, x3, x4, x5, x6, x7)  =  U32_gaaa(x1, x2, x7)
splitcD_out_ggaaa(x1, x2, x3, x4, x5)  =  splitcD_out_ggaaa(x1, x2, x3, x4)
MERGESORTB_IN_GAA(x1, x2, x3)  =  MERGESORTB_IN_GAA(x1)
U25_GAA(x1, x2, x3, x4, x5, x6, x7)  =  U25_GAA(x1, x2, x3, x7)

We have to consider all (P,R,Pi)-chains

(51) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(52) Obligation:

Q DP problem:
The TRS P consists of the following rules:

MERGESORTB_IN_GAA(.(X1, .(X2, X3))) → U25_GAA(X1, X2, X3, splitcD_in_ggaaa(X2, X3))
U25_GAA(X1, X2, X3, splitcD_out_ggaaa(X2, X3, X7, X8)) → MERGESORTB_IN_GAA(.(X1, X8))

The TRS R consists of the following rules:

splitcD_in_ggaaa(X1, X2) → U37_ggaaa(X1, X2, splitcA_in_gaaa(X2))
U37_ggaaa(X1, X2, splitcA_out_gaaa(X2, X4, X3)) → splitcD_out_ggaaa(X1, X2, .(X1, X3), X4)
splitcA_in_gaaa([]) → splitcA_out_gaaa([], [], [])
splitcA_in_gaaa(.(X1, X2)) → U32_gaaa(X1, X2, splitcA_in_gaaa(X2))
U32_gaaa(X1, X2, splitcA_out_gaaa(X2, X4, X3)) → splitcA_out_gaaa(.(X1, X2), .(X1, X3), X4)

The set Q consists of the following terms:

splitcD_in_ggaaa(x0, x1)
U37_ggaaa(x0, x1, x2)
splitcA_in_gaaa(x0)
U32_gaaa(x0, x1, x2)

We have to consider all (P,Q,R)-chains.

(53) Rewriting (EQUIVALENT transformation)

By rewriting [LPAR04] the rule MERGESORTB_IN_GAA(.(X1, .(X2, X3))) → U25_GAA(X1, X2, X3, splitcD_in_ggaaa(X2, X3)) at position [3] we obtained the following new rules [LPAR04]:

MERGESORTB_IN_GAA(.(X1, .(X2, X3))) → U25_GAA(X1, X2, X3, U37_ggaaa(X2, X3, splitcA_in_gaaa(X3)))

(54) Obligation:

Q DP problem:
The TRS P consists of the following rules:

U25_GAA(X1, X2, X3, splitcD_out_ggaaa(X2, X3, X7, X8)) → MERGESORTB_IN_GAA(.(X1, X8))
MERGESORTB_IN_GAA(.(X1, .(X2, X3))) → U25_GAA(X1, X2, X3, U37_ggaaa(X2, X3, splitcA_in_gaaa(X3)))

The TRS R consists of the following rules:

splitcD_in_ggaaa(X1, X2) → U37_ggaaa(X1, X2, splitcA_in_gaaa(X2))
U37_ggaaa(X1, X2, splitcA_out_gaaa(X2, X4, X3)) → splitcD_out_ggaaa(X1, X2, .(X1, X3), X4)
splitcA_in_gaaa([]) → splitcA_out_gaaa([], [], [])
splitcA_in_gaaa(.(X1, X2)) → U32_gaaa(X1, X2, splitcA_in_gaaa(X2))
U32_gaaa(X1, X2, splitcA_out_gaaa(X2, X4, X3)) → splitcA_out_gaaa(.(X1, X2), .(X1, X3), X4)

The set Q consists of the following terms:

splitcD_in_ggaaa(x0, x1)
U37_ggaaa(x0, x1, x2)
splitcA_in_gaaa(x0)
U32_gaaa(x0, x1, x2)

We have to consider all (P,Q,R)-chains.

(55) UsableRulesProof (EQUIVALENT transformation)

As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.

(56) Obligation:

Q DP problem:
The TRS P consists of the following rules:

U25_GAA(X1, X2, X3, splitcD_out_ggaaa(X2, X3, X7, X8)) → MERGESORTB_IN_GAA(.(X1, X8))
MERGESORTB_IN_GAA(.(X1, .(X2, X3))) → U25_GAA(X1, X2, X3, U37_ggaaa(X2, X3, splitcA_in_gaaa(X3)))

The TRS R consists of the following rules:

splitcA_in_gaaa([]) → splitcA_out_gaaa([], [], [])
splitcA_in_gaaa(.(X1, X2)) → U32_gaaa(X1, X2, splitcA_in_gaaa(X2))
U37_ggaaa(X1, X2, splitcA_out_gaaa(X2, X4, X3)) → splitcD_out_ggaaa(X1, X2, .(X1, X3), X4)
U32_gaaa(X1, X2, splitcA_out_gaaa(X2, X4, X3)) → splitcA_out_gaaa(.(X1, X2), .(X1, X3), X4)

The set Q consists of the following terms:

splitcD_in_ggaaa(x0, x1)
U37_ggaaa(x0, x1, x2)
splitcA_in_gaaa(x0)
U32_gaaa(x0, x1, x2)

We have to consider all (P,Q,R)-chains.

(57) QReductionProof (EQUIVALENT transformation)

We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].

splitcD_in_ggaaa(x0, x1)

(58) Obligation:

Q DP problem:
The TRS P consists of the following rules:

U25_GAA(X1, X2, X3, splitcD_out_ggaaa(X2, X3, X7, X8)) → MERGESORTB_IN_GAA(.(X1, X8))
MERGESORTB_IN_GAA(.(X1, .(X2, X3))) → U25_GAA(X1, X2, X3, U37_ggaaa(X2, X3, splitcA_in_gaaa(X3)))

The TRS R consists of the following rules:

splitcA_in_gaaa([]) → splitcA_out_gaaa([], [], [])
splitcA_in_gaaa(.(X1, X2)) → U32_gaaa(X1, X2, splitcA_in_gaaa(X2))
U37_ggaaa(X1, X2, splitcA_out_gaaa(X2, X4, X3)) → splitcD_out_ggaaa(X1, X2, .(X1, X3), X4)
U32_gaaa(X1, X2, splitcA_out_gaaa(X2, X4, X3)) → splitcA_out_gaaa(.(X1, X2), .(X1, X3), X4)

The set Q consists of the following terms:

U37_ggaaa(x0, x1, x2)
splitcA_in_gaaa(x0)
U32_gaaa(x0, x1, x2)

We have to consider all (P,Q,R)-chains.

(59) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04,JAR06].


The following pairs can be oriented strictly and are deleted.


MERGESORTB_IN_GAA(.(X1, .(X2, X3))) → U25_GAA(X1, X2, X3, U37_ggaaa(X2, X3, splitcA_in_gaaa(X3)))
The remaining pairs can at least be oriented weakly.
Used ordering: Polynomial interpretation [POLO]:

POL(.(x1, x2)) = 1 + x2   
POL(MERGESORTB_IN_GAA(x1)) = x1   
POL(U25_GAA(x1, x2, x3, x4)) = x4   
POL(U32_gaaa(x1, x2, x3)) = 1 + x3   
POL(U37_ggaaa(x1, x2, x3)) = 1 + x3   
POL([]) = 0   
POL(splitcA_in_gaaa(x1)) = x1   
POL(splitcA_out_gaaa(x1, x2, x3)) = x2 + x3   
POL(splitcD_out_ggaaa(x1, x2, x3, x4)) = 1 + x4   

The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented:

splitcA_in_gaaa([]) → splitcA_out_gaaa([], [], [])
splitcA_in_gaaa(.(X1, X2)) → U32_gaaa(X1, X2, splitcA_in_gaaa(X2))
U37_ggaaa(X1, X2, splitcA_out_gaaa(X2, X4, X3)) → splitcD_out_ggaaa(X1, X2, .(X1, X3), X4)
U32_gaaa(X1, X2, splitcA_out_gaaa(X2, X4, X3)) → splitcA_out_gaaa(.(X1, X2), .(X1, X3), X4)

(60) Obligation:

Q DP problem:
The TRS P consists of the following rules:

U25_GAA(X1, X2, X3, splitcD_out_ggaaa(X2, X3, X7, X8)) → MERGESORTB_IN_GAA(.(X1, X8))

The TRS R consists of the following rules:

splitcA_in_gaaa([]) → splitcA_out_gaaa([], [], [])
splitcA_in_gaaa(.(X1, X2)) → U32_gaaa(X1, X2, splitcA_in_gaaa(X2))
U37_ggaaa(X1, X2, splitcA_out_gaaa(X2, X4, X3)) → splitcD_out_ggaaa(X1, X2, .(X1, X3), X4)
U32_gaaa(X1, X2, splitcA_out_gaaa(X2, X4, X3)) → splitcA_out_gaaa(.(X1, X2), .(X1, X3), X4)

The set Q consists of the following terms:

U37_ggaaa(x0, x1, x2)
splitcA_in_gaaa(x0)
U32_gaaa(x0, x1, x2)

We have to consider all (P,Q,R)-chains.

(61) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs with 1 less node.

(62) TRUE